[isabelle-dev] Isabelle/jEdit -l
Makarius
makarius at sketis.net
Fri Sep 28 12:16:30 CEST 2012
On Fri, 28 Sep 2012, Christian Sternagel wrote:
> I assumed that everything that is listed by 'isabelle findlogics' would
> also be suitable for 'isabelle jedit -l'. However, currently if I first
> build an image from some local directory (i.e, having its own ROOT
> and/or ROOTS file(s)) - let's call it A - then 'isabelle jedit -l A'
> results in 'Undefined Session(s): "A"'. I need to explicitly state
> 'isabelle jedit -d . -l A' to make it work.
You have discovered that we are half-way in the transition to "logical
session names" (as in the isabelle build name space), instead of pointing
to the file-system (via findlogics).
See also
http://isabelle.in.tum.de/repos/isabelle/file/248e66e8321f/src/Tools/jEdit/src/isabelle_logic.scala#l72
There is still a slight mismatch: the outer syntax is determined
statically from the session information, and the image is then searched
again in some other way.
Makarius
More information about the isabelle-dev
mailing list