[isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Christian Sternagel]

Dear list,

I was just about to have a look at the latest and greatest Isabelle (
f35abc25d7b1 ) when I noticed the following behavior.

I started with

  isabelle jedit -bf

and then tried

  isabelle jedit -l HOL

but got an error message about missing files (see PS for details).

Now, these missing files are only referenced in IsaFoR's ROOT file (and
the reason for the error is that IsaFoR is still running on
Isabelle2006-1), which is read since IsaFoR is registered as an Isabelle
component in my "etc/settings"

I think it would be convenient if

1) sessions that are not ancestors of "-l Session" are not checked on
startup (or at least there was a way to activate this behavior),

2) or there was some easy way (e.g., a flag) to exclude specific
Isabelle components / sessions / ROOT files from checks (without having
to edit "etc/settings").

What do you think?

cheers

chris

PS: The exact error message was

/home/griff/repos/tools/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start:
*** No such file:
"/home/griff/repos/tools/isabelle/src/HOL/Library/Fraction_Field.thy"
*** The error(s) above occurred for theory "HOL-Lib.Fraction_Field"
(line 17 of "/home/griff/repos/isafor/thys/ROOT")
*** No such file:
"/home/griff/repos/tools/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy"
*** The error(s) above occurred for theory
"HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of
"/home/griff/repos/isafor/thys/ROOT")
*** No such file:
"/home/griff/repos/tools/isabelle/src/HOL/Library/Polynomial_Factorial.thy"
*** The error(s) above occurred for theory
"HOL-Lib.Polynomial_Factorial" (line 29 of
"/home/griff/repos/isafor/thys/ROOT")
*** The error(s) above occurred in session "HOL-Lib" (line 1 of
"/home/griff/repos/isafor/thys/ROOT")