# HG changeset patch
# User wenzelm
# Date 1330607538 -3600
# Node ID 852baa599351c62373ff06b148b733b2684d35b5
# Parent  6024353549ca0d8a75b1cf9c3947aff00eb10ed5
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;

diff -r 6024353549ca -r 852baa599351 src/Pure/System/swing_thread.scala
--- a/src/Pure/System/swing_thread.scala	Thu Mar 01 11:28:33 2012 +0100
+++ b/src/Pure/System/swing_thread.scala	Thu Mar 01 14:12:18 2012 +0100
@@ -45,7 +45,7 @@
 
   /* delayed actions */
 
-  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): () => Unit =
+  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
   {
     val listener = new ActionListener {
       override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
@@ -54,7 +54,9 @@
     timer.setRepeats(false)
 
     def invoke() { later { if (first) timer.start() else timer.restart() } }
-    invoke _
+    def revoke() { timer.stop() }
+
+    (active: Boolean) => if (active) invoke() else revoke()
   }
 
   // delayed action after first invocation
diff -r 6024353549ca -r 852baa599351 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 11:28:33 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 14:12:18 2012 +0100
@@ -111,12 +111,6 @@
       }
     }
 
-    def init()
-    {
-      flush()
-      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
-    }
-
     private val delay_flush =
       Swing_Thread.delay_last(session.input_delay) { flush() }
 
@@ -124,13 +118,25 @@
     {
       Swing_Thread.require()
       pending += edit
-      delay_flush()
+      delay_flush(true)
     }
 
     def update_perspective()
     {
       pending_perspective = true
-      delay_flush()
+      delay_flush(true)
+    }
+
+    def init()
+    {
+      flush()
+      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+    }
+
+    def exit()
+    {
+      delay_flush(false)
+      flush()
     }
   }
 
@@ -192,7 +198,7 @@
 
   private def deactivate()
   {
-    pending_edits.flush()
+    pending_edits.exit()
     buffer.removeBufferListener(buffer_listener)
     Token_Markup.refresh_buffer(buffer)
   }
diff -r 6024353549ca -r 852baa599351 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Mar 01 11:28:33 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Mar 01 14:12:18 2012 +0100
@@ -343,11 +343,13 @@
     update_snapshot().node.proper_command_at(text_area.getCaretPosition)
   }
 
-  private val caret_listener = new CaretListener {
-    private val delay = Swing_Thread.delay_last(session.input_delay) {
+  private val delay_caret_update =
+    Swing_Thread.delay_last(session.input_delay) {
       session.caret_focus.event(Session.Caret_Focus)
     }
-    override def caretUpdate(e: CaretEvent) { delay() }
+
+  private val caret_listener = new CaretListener {
+    override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
   }
 
 
@@ -373,7 +375,7 @@
             if (updated ||
                 (changed.nodes.contains(model.name) &&
                  changed.commands.exists(snapshot.node.commands.contains)))
-              overview.delay_repaint()
+              overview.delay_repaint(true)
 
             visible_range() match {
               case None =>
@@ -430,8 +432,8 @@
     text_area.removeFocusListener(focus_listener)
     text_area.getView.removeWindowListener(window_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
-    text_area.removeCaretListener(caret_listener)
-    text_area.removeLeftOfScrollBar(overview)
+    text_area.removeCaretListener(caret_listener); delay_caret_update(false)
+    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
     text_area.getGutter.removeExtension(gutter_painter)
     text_area_painter.deactivate()
     painter.removeExtension(tooltip_painter)
diff -r 6024353549ca -r 852baa599351 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Mar 01 11:28:33 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Mar 01 14:12:18 2012 +0100
@@ -126,14 +126,17 @@
     Isabelle.session.global_settings -= main_actor
     Isabelle.session.commands_changed -= main_actor
     Isabelle.session.caret_focus -= main_actor
+    delay_resize(false)
   }
 
 
   /* resize */
 
+  private val delay_resize =
+    Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
+
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
-    override def componentResized(e: ComponentEvent) { delay() }
+    override def componentResized(e: ComponentEvent) { delay_resize(true) }
   })
 
 
diff -r 6024353549ca -r 852baa599351 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Mar 01 11:28:33 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Mar 01 14:12:18 2012 +0100
@@ -390,9 +390,12 @@
 
             case Session.Ready =>
               Isabelle.jedit_buffers.foreach(Isabelle.init_model)
-              delay_load()
+              delay_load(true)
 
-            case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+            case Session.Shutdown =>
+              Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+              delay_load(false)
+
             case _ =>
           }
         case bad => System.err.println("session_manager: ignoring bad message " + bad)
@@ -416,7 +419,7 @@
         if (Isabelle.session.is_ready) {
           val buffer = msg.getBuffer
           if (buffer != null) Isabelle.init_model(buffer)
-          delay_load()
+          delay_load(true)
         }
 
       case msg: EditPaneUpdate