Thanks Lars! I did not yet try your suggestion (and I am somewhat reluctant to install "3rd party" software for something I would consider basic functionality; but anyway, it's good to know that there is an alternative).
Thanks Makarius! I even read the email you are referring to, but apparently this was too long ago ;) Anyway, what you suggest does in principle work (and shows that all the required functionality is already there). With isabelle jedit -R -l HOL I end up in Isabelle/HOL's ROOT file and everything after Pure has to be loaded. I am curious, is there a reason why it would not be a good idea to restrict to Session by default whenever isabelle jedit -l Sessions is invoked? Alternatively, something similar to "-R" but where I do not end up in a ROOT file and the specified session is already built (but none of its descendants is checked) might be convenient. cheers chris On 05/18/2017 10:34 AM, Makarius wrote: > On 18/05/17 09:03, Christian Sternagel wrote: >> >> 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" > > See > http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07321.html > > Quote: > > In current Isabelle/6acb28e5ba41 it is also possible to use something > like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space > to the requirements of MY_SESSION. > > > Makarius > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev