# HG changeset patch
# User immler@in.tum.de
# Date 1229355259 -3600
# Node ID a67a4eaebcff5c2121e8068fc7f889e838b40ea6
# Parent  98155c35d252a24d4cb080b6f441e43f581cdbef
added 'delay or ignore'

diff -r 98155c35d252 -r a67a4eaebcff src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 15 16:23:17 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 15 16:34:19 2008 +0100
@@ -39,9 +39,7 @@
 	private val HILITE_HEIGHT = 2
 
   Plugin.plugin.prover.commandInfo.add(cc => {
-      System.err.println(cc.command.idString + ": " + cc.command.phase)
       paintCommand(cc.command,textarea.getBuffer, getGraphics)
-      System.err.println(cc.command.idString + ": " + cc.command.phase)
     })
   setRequestFocusEnabled(false);
 
diff -r 98155c35d252 -r a67a4eaebcff src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Dec 15 16:23:17 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Dec 15 16:34:19 2008 +0100
@@ -96,8 +96,9 @@
     buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
 
     val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
-    prover.commandInfo.add(_ => repaint_delay.delay())
-    
+    prover.commandInfo.add(_ => repaint_delay.delay_or_ignore())
+    // could also use this:
+    // prover.commandInfo.add(c => repaint(c.command))
     Plugin.plugin.viewFontChanged.add(font => updateFont())
     
     colTimer.stop
diff -r 98155c35d252 -r a67a4eaebcff src/Tools/jEdit/src/utils/Delay.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/utils/Delay.scala	Mon Dec 15 16:34:19 2008 +0100
@@ -0,0 +1,21 @@
+package isabelle.utils
+
+import javax.swing.Timer
+import java.awt.event.{ActionListener, ActionEvent}
+
+class Delay(amount : Int, action : () => Unit) {
+
+  val timer : Timer = new Timer(amount, new ActionListener {
+      override def actionPerformed(e:ActionEvent){
+        action ()
+      }
+    })
+  // if called very often, action is executed at most once
+  // in amount milliseconds
+  def delay_or_ignore () = {
+    if (! timer.isRunning()){
+      timer.setRepeats(false)
+      timer.start()
+    }
+  }
+}