Just an observation. Assuming that the grayish background highlighting
really indicates prover activity in the background, I recently noticed
that sometimes a "re-check" of the whole buffer is done in situations
where this is (as far as I see) not necessary. For example, having
lemma "..."
by auto
lemma "..."
by auto
when I select the second "by auto" (typically S+Home, since the courser
is positioned directly behind it after just having typed it) and then
replace the selected region by something different, the whole buffer is
highlighted (thus re-chekced or re-parsed?).
This is not the only such situation, but one that I could reproduce
reliably.
Note also that -- just making a subjective evaluation by "feeling" --
that this "re-checking" happens more frequently in a1cd4126a1c4 (and
possibly earlier) than in Isabelle2013.
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
