[isabelle-dev] Reprocessing in Isabelle/jEdit

[Makarius]

On Tue, 24 Mar 2015, Jasmin Blanchette wrote:

> When editing inside Isabelle/jEdit (f19f4afa49e2), it used to be so that 
> everything above was left alone. Now, if I edit a lemma in the middle of 
> the window, everything above it that is visible gets reprocessed.

This is certainly bad.  Strange that it did not show up earlier: bisection 
shows it is from 12 days ago:

The first bad revision is:
changeset:   59678:86a76300137e
user:        wenzelm
date:        Thu Mar 12 20:34:08 2015 +0100
summary:     clarified command content;

When doing this I was aware of the importance of proper command comparison 
for the editing process, but got it wrong nonetheless due to weakly-typed 
equality in Java/Scala!  I stared a long time at the sources, without 
seeing it -- I am used to think in strongly-typed ML.

This lapse is now addressed in the subsequent change:

changeset:   59801:88a89f01fc27
user:        wenzelm
date:        Tue Mar 24 23:37:05 2015 +0100
files:       src/Pure/Thy/thy_syntax.scala
description:
proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

--- a/src/Pure/Thy/thy_syntax.scala	Tue Mar 24 21:54:25 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Mar 24 23:37:05 2015 +0100
@@ -147,8 +147,8 @@
      : (List[Command], List[(Command.Blobs_Info, Command_Span.Span)]) =
    {
      (cmds, blobs_spans) match {
-      case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
-        chop_common(cmds, rest)
+      case (cmd :: cmds, (blobs_info, span) :: rest)
+      if cmd.blobs_info == blobs_info && cmd.span == span => chop_common(cmds, rest)
        case _ => (cmds, blobs_spans)
      }
    }


 	Makarius