[isabelle-dev] jEdit

[Makarius]

On Wed, 2 May 2012, Christian Sternagel wrote:

> would it make sense to introduce some kind of "read-only" mode for 
> theory files and then use this mode when jumping to a file that is 
> already finished (instead of the "Attempt to update loaded theory ..." 
> error message)?
>
> Of course I don't know whether it is easily possible to distinguish 
> between files that are already loaded as part of a heap image and files 
> that are loaded by hand (which should not be loaded in read-only mode).
>
> On a related note: the output of such loaded files is still interesting. 
> Is there any way to make the output immediately available from the heap 
> image, without actually loading the theory (in the end it was already 
> loaded when creating the heap image, but I guess the output is a 
> side-effect and not part of the resulting heap)?

This all makes sense, and is in the pipe-line for a long time already.

It is all about reforming the old theory loader (and its batch mode) to 
converge it with the interactive document model that is now seen in the 
Prover IDE.

It will probably take a bit more time to get there, extrapolating from the 
slow progress of the past 4 years.


 	Makarius