> Am 05.06.2018 um 14:47 schrieb Makarius <makar...@sketis.net>: > > 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? In this particular case, it was a relatively short theory (300 lines) with no long-running or non-terminating commands. I inserted and removed some diagnostic commands (code_thms, export_code foo in SML), but those were not present anymore when I observed this 4-second-consolidation-loop.
Fabian
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
