[isabelle-dev] Remaining uses of Proof General?

Makarius makarius at sketis.net
Sat May 24 13:25:36 CEST 2014


This is not a remaining use of Proof General, but of the Emacs text 
editor: trimming the final newline of theory sources for document 
preparation.  This could lead to extra white space between sections in the 
last decades, but it was just one of these habits to take care of that 
manually.

jEdit has its own built-in "smartness" concerning the last line, and some 
well-known problems coming from it, especially for plugin authors who need 
to paint something into the text buffer.  Since there is no realistic 
chance to remove superfluous newlines manually, Isabelle/5fc1c2098964 now 
does that unconditionally during document preparation.

(For now the list of Remaining uses of Proof General / Emacs seems to be 
empty.  If there is anything remaining, this thread is still open to 
submissions.)


 	Makarius



More information about the isabelle-dev mailing list