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