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?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
