Re: [isabelle] Isabelle2015-RC3 available for testing: Overzealous reprocessing



On Thu, 7 May 2015, Lars Noschinski wrote:

On 07.05.2015 11:32, Makarius wrote:
On Thu, 7 May 2015, Lars Noschinski wrote:

I'm currently cleaning up some of my theories. Sometimes, when
changing stuff in the middle of a theory, Isabelle starts
reprocessing all loaded theories (everything becomes pink again).

I observed this first when there where quite a numbers of failed
proofs on the way to the position I changed. But I could also trigger
this behavior if all proofs go through.

This often happened shortly after I did a hypersearch over all open
buffers while Isabelle was busy (but this observation might be
confirmation-biased).

Do you have any auxiliary files in that development, i.e. ML_file? If
such a file changes its status from non-open to open, everything
following it will be re-checked.
There are some auxiliary files, yes. But searching in "all buffers"
should not open any new buffer, shouldn't it? (And I am pretty sure I
did not open any of these files manually).

I've had a look at the Isabelle/Scala sources, to see when a virtual "reload" of the document happens: there is a second possibility, due to change of buffer syntax (which is now local to each buffer in Isabelle2015).

In https://bitbucket.org/isabelle_project/isabelle-release/commits/c2837a39da01 this situation no longer causes spurious edits of the document content.

This will be in the next release candidate within a few days.


	Makarius





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