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