Re: [isabelle-dev] Reprocessing in Isabelle/jEdit
I noticed the same behaviour yesterday, with fe5b796d6b2a. This is very inconvenient, in particular if you have long-lasting proof methods or big goal outputs, this produces lots of additional load. -- Peter On Di, 2015-03-24 at 13:29 +0100, Jasmin Blanchette wrote: Hi all, 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. So if I write something like thm list.exhaust it can take a couple of seconds before I get feedback, if there’s some heavy material preceding it. I noticed this behavior for the first time last week or so — so did Mathias Fleury. We’re both using Macs. Is this behavior intentional? Is there a way to get the old, much more responsive behavior back? Thanks. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Reprocessing in Isabelle/jEdit
Hi all, 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. So if I write something like thm list.exhaust it can take a couple of seconds before I get feedback, if there’s some heavy material preceding it. I noticed this behavior for the first time last week or so — so did Mathias Fleury. We’re both using Macs. Is this behavior intentional? Is there a way to get the old, much more responsive behavior back? Thanks. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reprocessing in Isabelle/jEdit
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
