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

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 this situation no longer causes spurious edits of the document content.

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


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