# HG changeset patch
# User wenzelm
# Date 1438784022 -7200
# Node ID 9980f3bcdea2be5978a8b33d429ba0779d58a4f2
# Parent  5510c8444bc41692f31881aa2c99761c5599de9f
tuned signature;

diff -r 5510c8444bc4 -r 9980f3bcdea2 etc/options
--- a/etc/options	Wed Aug 05 14:18:07 2015 +0200
+++ b/etc/options	Wed Aug 05 16:13:42 2015 +0200
@@ -111,7 +111,7 @@
   -- "ML debugger in single-step mode"
 
 public option ML_statistics : bool = true
-  -- "ML runtime system statistics"
+  -- "ML run-time system statistics"
 
 
 section "Editor Reactivity"
diff -r 5510c8444bc4 -r 9980f3bcdea2 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Aug 05 14:18:07 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Aug 05 16:13:42 2015 +0200
@@ -201,24 +201,8 @@
 
   /* ML statistics */
 
-  private val ML_STATISTICS = "ML_statistics"
-
-  def ml_statistics: Boolean = PIDE.options.bool(ML_STATISTICS)
-  def ml_statistics_=(b: Boolean): Unit =
-    GUI_Thread.require {
-      if (ml_statistics != b) {
-        PIDE.options.bool(ML_STATISTICS) = b
-        PIDE.session.update_options(PIDE.options.value)
-      }
-    }
-
-  class ML_Stats extends CheckBox("ML statistics")
-  {
-    tooltip = "Enable ML runtime system statistics"
-    reactions += { case ButtonClicked(_) => ml_statistics = selected }
-    def load() { selected = ml_statistics }
-    load()
-  }
+  class ML_Stats extends
+    JEdit_Options.Check_Box("ML_statistics", "ML statistics", "Enable ML runtime system statistics")
 
 
   /* required document nodes */
diff -r 5510c8444bc4 -r 9980f3bcdea2 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Aug 05 14:18:07 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Aug 05 16:13:42 2015 +0200
@@ -14,6 +14,7 @@
 import javax.swing.text.JTextComponent
 
 import scala.swing.{Component, CheckBox, TextArea}
+import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.gui.ColorWellButton
 
@@ -28,6 +29,23 @@
 object JEdit_Options
 {
   val RENDERING_SECTION = "Rendering of Document Content"
+
+  class Check_Box(name: String, label: String, description: String) extends CheckBox(label)
+  {
+    tooltip = description
+    reactions += { case ButtonClicked(_) => update(selected) }
+
+    def stored: Boolean = PIDE.options.bool(name)
+    def load() { selected = stored }
+    def update(b: Boolean): Unit =
+      GUI_Thread.require {
+        if (selected != b) selected = b
+        if (stored != b) {
+          PIDE.options.bool(name) = b
+          PIDE.session.update_options(PIDE.options.value)
+        }
+      }
+  }
 }
 
 class JEdit_Options extends Options_Variable