Re: [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
___
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

[Peter Lammich]

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

[Jasmin Blanchette]

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