[isabelle-dev] jEdit: re-checking of main buffer

[Christian Sternagel]

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