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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
