[isabelle-dev] Remaining uses of Proof General?

Makarius makarius at sketis.net
Fri Jun 27 14:02:24 CEST 2014


On Fri, 27 Jun 2014, Peter Lammich wrote:

> * Isabelle/jEdit cannot open a theory-file without processing it. This
> is in particular a problem when porting stuff and opening the original
> version of the same file to look something up. Even worse: Once opened,
> you cannot close the file again, and it will remain in the theory panel
> (with an error marker) until you quit jEdit.

You can in principle switch off the continous checking, e.g. in the 
Theories panel.

Slight inconveniences and potential for improvements remain, but this is 
no show stopper as far as I can tell.


 	Makarius



More information about the isabelle-dev mailing list