[isabelle] Isabelle/jEdit - default logic



Dear all,

1) First a trivial observation: When I start Isabelle/jEdit via

  isabelle jedit -d .

and the current directory contains a ROOT file with a session FOO, then the logic selector in the theory panel will contain the session FOO.

If I do the same via

  isabelle jedit

FOO is not there, which is expected.

Now, after doing

  isabelle build -d . -b FOO

there is the heap image FOO in my ~/.isabelle/Isabelle2013-2/heaps/... but nevertheless the logic selector will not contain FOO when starting jEdit via

  isabelle jedit

Again, this is as expected.

2) Now I was wondering about the following: For users that start Isabelle/jEdit via clicking on an icon, which is I guess equivalent to doing

  $ISABELLE_HOME/Isabelle2013-2

on a console. How are they expected to access FOO as default logic? Maybe the logic selector should provide all images that are present in ISABELLE_PATH ? But then again, how are GUI-only users expected to build FOO in the first place? Maybe it would be good to have something like the former "build_dialog" that can be started from within Isabelle/jEdit?

cheers

chris




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