On 05/06/18 14:45, Fabian Immler wrote:
>>> The only way to stop this apparently is to invalidate something in the
>>> beginning of the (currently open) theory.
>> It should be possible to achieve this effect by removing the concluding
>> 'end' command.
> Just now I was in the middle of a theory (without any 'end' command), where 
> every (are they supposed to happen periodically?) "consolidation" took about 
> 4 seconds.
> It seems like something is accumulating somewhere when editing the document, 
> because after invalidating the beginning of the theory and going back to the 
> same place as before, the "consolidation" was not noticeable any more.

What kind of theory is this? Many commands? Long-running /
non-terminating commands?


isabelle-dev mailing list

Reply via email to