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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
