On 18/05/17 11:13, Christian Sternagel wrote:
>
> 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.
The option -R has another purpose: it reinterprets -l to refer to the
requirements of that session. It means you actually need to specify the
session that you are going to edit.
There is some extra complication behind -R and -l that might see more
refinement eventually, but it is probably better to move all that
session selection functionality into the IDE.
> 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?
Some weeks ago I have started to move into the other direction. This is
all motivated by the session-qualified theory names reform, which has
been postponed several years already.
When that is fully active, it means that the PIDE can edit any source
file you like and know to which session it belongs.
Further fine points might still need polishing. I hope we manage that
during the summer, such that it all works smoothly for the Isabelle2017
release.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
