# Re: [isabelle] Isabelle2014-RC0: phantom theories

On Tue, 8 Jul 2014, Christian Sternagel wrote:


3) Now after the plus-sign enter the usual

theory Test
imports M
begin
end


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.


I think this is just a consequence of the normal operation of creating PIDE document nodes from buffers, non-buffers, not-yet-buffers, no-longer-buffers. The Isabelle/jEdit manual has this slightly cryptic entry in the last chapter, which is related, but does not tell the whole story:

\item \textbf{Problem:} No way to delete document nodes from the overall
collection of theories.

\textbf{Workaround:} Ignore unused files.  Restart whole
Isabelle/jEdit session in worst-case situation.


These mechanisms date back several years, and I did not have time yet to brush them up. Anything that touches theory import management usually causes entanglement in the "4 modes of Isabelle", as explained earlier on this thread.


Makarius



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.