[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