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
This archive was generated by a fusion of
Pipermail (Mailman edition) and