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

[Christian Sternagel]

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
>