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") _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev