Email Gateway (Aug 22 2022 at 09:42): Email Gateway (Aug 22 2022 at 09:42):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 10:08):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
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).
-- Lars
Email Gateway (Aug 22 2022 at 10:09):From: Makarius <makarius@sketis.net>
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.
I just want to make sure that there is a real problem, and not the
situation that is documented in the "jedit" manual in the section 3.1.3
"Auxiliary files".
Makarius
Email Gateway (Aug 22 2022 at 10:09):From: Lars Noschinski <noschinl@in.tum.de>
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).
-- Lars
Last updated: Apr 25 2024 at 08:20 UTC