[isabelle-dev] Isabelle/jEdit -l

Christian Sternagel c-sterna at jaist.ac.jp
Fri Sep 28 09:22:33 CEST 2012


If I'm not mistaken the -l flag slightly changed its semantics somewhen 
in the recent past?

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.

Now I'm curious. Since currently all images are generated into the same 
directory ISABELLE_OUTPUT (and thus, images having the same name would 
override each other), why is it useful to have a distinction when 
starting jedit? Maybe in the future images will not end up at the same 
place? Or is the current behavior not intended?

cheers

chris


More information about the isabelle-dev mailing list