Re: [isabelle] The instructions in AFP's "Using Entries" do not work



On 06/06/2021 02:35, Gerwin Klein wrote:
> 
>> On 6 Jun 2021, at 06:00, Makarius <makarius at sketis.net> wrote:
> 
>> The option -d '$AFP' has later become idiomatic for many other Isabelle tools,
>> to add the "AFP aspect" with minimal complexity. For example for the Prover IDE:
>>
>>  isabelle jedit -d '$AFP'
> 
> Agree, that was the canonical way, but that was part of the problem. It doesn't work for users who don't use the command line.

Yes, I am aware of that extra assumption. It is part of the process to rethink
AFP within the Prover IDE.

There is another ongoing process of rethinking: how to allow Isabelle/Scala
modules within sessions and/or components.

Maybe I eventually get the right idea, when revisiting this more seriously.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.