[isabelle] Isabelle2014-RC0: phantom theories
I sometimes notice that the theory panel on Isabelle/jEdit lists
theory-nodes that do not exist (and never did). Finally, I was able to
construct a minimal example (but it often happened to me when editing
the headers of real theory files). On my machine (x86_64-linux; Fedora
20) I can somewhat reliably reconstruct the issue as follows:
1) From the command line start Isabelle/jEdit with new file, e.g.,
isabelle jedit Test.thy
2) In the first line, enter a symbol that will cause an error, e.g., "+".
3) Now after the plus-sign enter the usual
where the imports consist of the non-existent theory M.
4) Go to the first line and delete it.
5) Open the theory panel, which no contains entries for "Test" and "M".
Note that I'm unable to reproduce the above, when the theory panel is
already open on startup of Isabelle/jEdit.
While I'm at it, another thing (but I guess this is well-known): In
IsaFoR we have a session HOL-AFP which builds a heap-image containing
all AFP entries we rely on. After building this image it is possible to
open (with Isabelle/jEdit) a file as follows
isabelle jedit -d . -l HOL-AFP Some_File.thy
that contains an import like
and there is no error-message (note that theory Misc exists, but at a
different location). When I try
isabelle jedit -d . Some_File.thy
instead and let Isabelle/jEdit figure out the dependencies itself
without any intermediate heap-images, then I obtain the error that the
above file does not exist. This asymmetry between using and not using a
heamp-image seems a bit awkward (although it is not clear to me whether
it can be avoided in general).
This archive was generated by a fusion of
Pipermail (Mailman edition) and