[isabelle-dev] jEdit import theories

[Makarius]

On Wed, 21 Mar 2012, Christian Sternagel wrote:

> Is it just me or is Isabelle/jEdit really much faster than 
> ProofGeneral/emacs when loading theories? (Maybe this is due to some 
> other difference between Isabelle2011-1 and the repo version; I only use 
> emacs if I have to stick to Isabelle2011-1.)

Ça depend, as the French like to say.

Isabelle/jEdit in Isabelle2011-1 and repository versions until today 
(8e1b14bf0190) uses a uniform model to process buffer content, intermixed 
with potential user edits, with full document markup reports that 
eventually causes the "Haribo effect" in the sources.  This is done in a 
reasonably fast way, but there are still situations where too many goal 
states are printed and thus the prover session gets overloaded.  (E.g. in 
Hoare_Parallel or AFP/JinjaThreads.)

In contrast, Proof General / Emacs is very slow in processing the current 
buffer (especially on Mac OS), but resolves imports via the batch-mode 
theory loader of Isabelle, which is presently faster than any other way of 
processing theories.  (The same is used for isabelle usedir/make/makeall.)

The general direction is to unify old-style batch loading with new-style 
document processing, such that it is both very fast and produces the full 
markup.  It will also overcome occasional confusions about different 
behaviour of tools in different modes of theory processing.


 	Makarius