Just to note, I'm adding a configuration option to force the use of the existing Emacs mode, so Prooftree will always be available.
-- Paul On May 13, 2016 11:08, "Pierre Courtieu" <pierre.court...@cnam.fr> wrote: > 2016-05-13 9:49 GMT+02:00 Hendrik Tews <hendrik.t...@fireeye.com>: > > For 2 and 5 I insert additional print commands into the queue of > > commands. Because you cannot print wrt. an old state, these print > > commands need to be inserted directly after the command that > > generates additional subgoals or that instantiate existential > > variables. > > This might change with the idesave + Stm protocol. > > Paul are you using the Stm stuff? > > P. > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
