[isabelle-dev] jEdit

[Christian Sternagel]

Dear Makarius,

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)?

cheers

chris