Re: [isabelle] Isabelle/jEdit - default logic
On Mon, 20 Jan 2014, Christian Sternagel wrote:
isabelle jedit -d .
isabelle build -d . -b FOO
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
on a console. How are they expected to access FOO as default logic?
The command lines of "isabelle jedit" and "isabelle build" coincide on
some options to manage the session name space and select logic images.
See also the description of "isabelle build" in the system manual. It has
the following additional explanation of option -d:
Any session root directory may refer recursively to further directories
of the same kind, by listing them in a catalog file ROOTS line-by-line.
This helps to organize large collections of session specifications, or
to make -d command line options persistent (say within
Maybe the logic selector should provide all images that are present in
The ISABELLE_PATH does not account for the session name space, it is
merely a way to find potential heap images in the file-system. Note that
this is in contrast to very ancient modes of operation of
isabelle-process, isabelle findlogics, and Proof General.
But then again, how are GUI-only users expected to build FOO in the
By using $ISABELLE_HOME_USER/ROOTS mentioned above. In principle the
Prover IDE should provide more direct access to ROOTS at some point, but
this is not implemented yet.
I get myself occasionally confused about the new toplevel application
wrappers, which are available on all platforms in Isabelle2013-2. Since I
am rarely in the privileged situation to use Isabelle as regular user, I
usually have old-fashioned "isabelle jedit" invocations on the
command-line, with slightly different semantics.
Maybe it would be good to have something like the former "build_dialog"
that can be started from within Isabelle/jEdit?
The build_dialog was just an intermediate thing, to help a hypothecial
Proof General maintainer to do what Isabelle/jEdit also does by itself via
isabelle.Build in Isabelle/Scala. Since no Proof General maintainer
showed up in such a long time, I have removed the "build_dialog" shell
script wrapper for Isabelle2013-2.
This archive was generated by a fusion of
Pipermail (Mailman edition) and