[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?



More information about the isabelle-dev mailing list