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.