[isabelle-dev] Isabelle/jEdit -l
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