[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