# HG changeset patch
# User wenzelm
# Date 1347019134 -7200
# Node ID 9d10bd85c1be74065b4f15c4c449eb4a1b1d479b
# Parent  85116a86d99f600d66a7c3719fc07c53021fa942
more explicit Delay operations;

diff -r 85116a86d99f -r 9d10bd85c1be src/Pure/System/swing_thread.scala
--- a/src/Pure/System/swing_thread.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Pure/System/swing_thread.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -47,19 +47,37 @@
 
   /* delayed actions */
 
-  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
+  abstract class Delay extends
   {
-    val listener = new ActionListener {
-      override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
+    def invoke(): Unit
+    def revoke(): Unit
+  }
+
+  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Delay =
+    new Delay {
+      private val timer = new Timer(time.ms.toInt, null)
+      timer.setRepeats(false)
+      timer.addActionListener(new ActionListener {
+        override def actionPerformed(e: ActionEvent) {
+          assert()
+          timer.setDelay(time.ms.toInt)
+          action
+        }
+      })
+
+      def invoke()
+      {
+        require()
+        if (first) timer.start() else timer.restart()
+      }
+
+      def revoke()
+      {
+        require()
+        timer.stop()
+        timer.setDelay(time.ms.toInt)
+      }
     }
-    val timer = new Timer(time.ms.toInt, listener)
-    timer.setRepeats(false)
-
-    def invoke() { later { if (first) timer.start() else timer.restart() } }
-    def revoke() { timer.stop() }
-
-    (active: Boolean) => if (active) invoke() else revoke()
-  }
 
   // delayed action after first invocation
   def delay_first = delayed_action(true) _
diff -r 85116a86d99f -r 9d10bd85c1be src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -121,12 +121,12 @@
     {
       Swing_Thread.require()
       pending += edit
-      delay_flush(true)
+      delay_flush.invoke()
     }
 
     def update_perspective()
     {
-      delay_flush(true)
+      delay_flush.invoke()
     }
 
     def init()
@@ -137,7 +137,7 @@
 
     def exit()
     {
-      delay_flush(false)
+      delay_flush.revoke()
       flush()
     }
   }
diff -r 85116a86d99f -r 9d10bd85c1be src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -346,7 +346,7 @@
     }
 
   private val caret_listener = new CaretListener {
-    override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
+    override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
   }
 
 
@@ -374,7 +374,7 @@
                 if (changed.assignment ||
                     (changed.nodes.contains(model.name) &&
                      changed.commands.exists(snapshot.node.commands.contains)))
-                  overview.delay_repaint(true)
+                  overview.delay_repaint.invoke()
 
                 visible_range() match {
                   case Some(visible) =>
@@ -435,8 +435,8 @@
     text_area.getView.removeWindowListener(window_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
     painter.removeMouseListener(mouse_listener)
-    text_area.removeCaretListener(caret_listener); delay_caret_update(false)
-    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
+    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
+    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
     text_area.getGutter.removeExtension(gutter_painter)
     text_area_painter.deactivate()
     painter.removeExtension(tooltip_painter)
diff -r 85116a86d99f -r 9d10bd85c1be src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -141,7 +141,7 @@
     Isabelle.session.global_settings -= main_actor
     Isabelle.session.commands_changed -= main_actor
     Isabelle.session.caret_focus -= main_actor
-    delay_resize(false)
+    delay_resize.revoke()
   }
 
 
@@ -151,7 +151,7 @@
     Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize(true) }
+    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   })
 
 
diff -r 85116a86d99f -r 9d10bd85c1be src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -416,11 +416,11 @@
 
             case Session.Ready =>
               Isabelle.jedit_buffers.foreach(Isabelle.init_model)
-              delay_load(true)
+              Swing_Thread.later { delay_load.invoke() }
 
             case Session.Shutdown =>
               Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
-              delay_load(false)
+              Swing_Thread.later { delay_load.revoke() }
 
             case _ =>
           }
@@ -458,7 +458,7 @@
           if (Isabelle.session.is_ready) {
             val buffer = msg.getBuffer
             if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
-            delay_load(true)
+            Swing_Thread.later { delay_load.invoke() }
           }
 
         case msg: EditPaneUpdate