[isabelle-dev] Outdated state after opening theories from images

Dmitriy Traytel traytel at in.tum.de
Sat Nov 23 08:53:04 CET 2013


Am 22.11.2013 21:40, schrieb Makarius:
> On Fri, 22 Nov 2013, Dmitriy Traytel wrote:
>
>> This refers to Isabelle/d71c2737ee21.
>>
>> The minimal example is really minimal this time:
>>
>> theory Scratch
>> imports Main
>> begin
>>
>> end
>>
>> In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a 
>> moment for the text to turn #EEE3E3, close Main.thy and Scratch.thy 
>> is now outdated as well. The only thing that helps now is a jEdit 
>> restart.
>
> That is a hard crash of the PIDE protocol handler in Isabelle/ML. It 
> should now work better with 31844ca390ad.
>
> This is a follow-up to the recently added support for auxiliary files 
> (via 'ML_file' etc.) within the Prover IDE (05738b7d8191 and before).

Thanks for the patch and the very useful feature for people working with 
Isabelle/ML.

Dmitriy




More information about the isabelle-dev mailing list