--- 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);
--- 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
--- /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()
+ }
+ }
+}