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

Makarius makarius at sketis.net
Fri Nov 22 21:40:58 CET 2013


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).


 	Makarius



More information about the isabelle-dev mailing list