Re: [isabelle] RC1 - Greyout



On Tue, 2 Feb 2016, Manuel Eberl wrote:

Another recurring problem that I noticed is that sometimes, when loading e.g. HOL, if one jumps into the middle of one of the theories to be built while the theories have not all finished building, Isabelle will start building /all/ of them from the beginning /again/.

This should normally happen only when the responsibility of 'ML_file' sources changes from prover to editor. When you click on a source file for the first time, overall checking recommences at that point.

That is a concession to resource usage. If everything would be managed by the editor by default, the HOL session could no longer be edited in 8GB memory.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.