# HG changeset patch
# User wenzelm
# Date 1448647227 -3600
# Node ID 814bbe5d92041448707df78e312e86a0a09e833e
# Parent  7f530d7e552dd94efafa79097213701a319db5a3# Parent  aa7b748bd96ccb579c9bb0a6ee7af62ecb788753
merged

diff -r 7f530d7e552d -r 814bbe5d9204 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Nov 27 18:01:13 2015 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Nov 27 19:00:27 2015 +0100
@@ -13,7 +13,7 @@
 
 import scala.collection.immutable.Queue
 import scala.swing.{TextArea, TextField, ScrollPane, Component, ComboBox, Button}
-import scala.swing.event.{SelectionChanged, ButtonClicked}
+import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged}
 
 import org.jfree.chart.ChartPanel
 import org.jfree.data.xy.XYSeriesCollection
@@ -57,7 +57,10 @@
       case Some((_, fields)) => ML_Statistics("", statistics.toList).update_data(data, fields)
     }
 
-  private val delay_update =
+  private val input_delay =
+    GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart }
+
+  private val update_delay =
     GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
 
 
@@ -89,6 +92,7 @@
     tooltip = "Limit for accumulated data"
     verifier = (s: String) =>
       s match { case Properties.Value.Int(x) => x > 0 case _ => false }
+    reactions += { case ValueChanged(_) => input_delay.invoke() }
   }
 
   private val controls =
@@ -107,7 +111,7 @@
     Session.Consumer[Any](getClass.getName) {
       case stats: Session.Statistics =>
         add_statistics(stats.props)
-        delay_update.invoke()
+        update_delay.invoke()
 
       case _: Session.Global_Options =>
         GUI_Thread.later { ml_stats.load() }
diff -r 7f530d7e552d -r 814bbe5d9204 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Nov 27 18:01:13 2015 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Nov 27 19:00:27 2015 +0100
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import scala.swing.{Button, Component, Label, TextField, CheckBox}
+import scala.swing.{Button, Component, Label, CheckBox}
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout