GUI controls for ML_statistics, for more digestible protocol dump;

--- a/etc/options	Wed Apr 15 11:47:29 2015 +0200
+++ b/etc/options	Wed Apr 15 13:55:01 2015 +0200
@@ -101,6 +101,9 @@
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
+public option ML_statistics : bool = true
+  -- "ML runtime system statistics"
+
 
 section "Editor Reactivity"
 

--- a/src/Pure/PIDE/protocol.ML	Wed Apr 15 11:47:29 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML	Wed Apr 15 13:55:01 2015 +0200
@@ -16,7 +16,7 @@
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
         Options.set_default options;
-        Future.ML_statistics := true;
+        Future.ML_statistics := Options.bool options "ML_statistics";
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads_update (Options.int options "threads");
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)

--- a/src/Tools/jEdit/src/isabelle.scala	Wed Apr 15 11:47:29 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Apr 15 13:55:01 2015 +0200
@@ -173,17 +173,14 @@
   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
 
   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
-
-  def continuous_checking_=(b: Boolean)
-  {
-    GUI_Thread.require {}
-
-    if (continuous_checking != b) {
-      PIDE.options.bool(CONTINUOUS_CHECKING) = b
-      PIDE.options_changed()
-      PIDE.editor.flush()
+  def continuous_checking_=(b: Boolean): Unit =
+    GUI_Thread.require {
+      if (continuous_checking != b) {
+        PIDE.options.bool(CONTINUOUS_CHECKING) = b
+        PIDE.options_changed()
+        PIDE.editor.flush()
+      }
     }
-  }
 
   def set_continuous_checking() { continuous_checking = true }
   def reset_continuous_checking() { continuous_checking = false }
@@ -198,6 +195,28 @@
   }
 
 
+  /* 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()
+  }
+
+
   /* required document nodes */
 
   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)

--- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Apr 15 11:47:29 2015 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed Apr 15 13:55:01 2015 +0200
@@ -44,6 +44,8 @@
 
   /* controls */
 
+  private val ml_stats = new Isabelle.ML_Stats
+
   private val select_data = new ComboBox[String](
     ML_Statistics.standard_fields.map(_._1))
   {
@@ -65,7 +67,8 @@
     }
   }
 
-  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
+  private val controls =
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data)
 
 
   /* layout */
@@ -77,13 +80,24 @@
   /* main */
 
   private val main =
-    Session.Consumer[Session.Statistics](getClass.getName) {
-      case stats =>
+    Session.Consumer[Any](getClass.getName) {
+      case stats: Session.Statistics =>
         rev_stats.change(stats.props :: _)
         delay_update.invoke()
+
+      case _: Session.Global_Options =>
+        GUI_Thread.later { ml_stats.load() }
     }
 
-  override def init() { PIDE.session.statistics += main }
-  override def exit() { PIDE.session.statistics -= main }
+  override def init()
+  {
+    PIDE.session.statistics += main
+    PIDE.session.global_options += main
+  }
+
+  override def exit()
+  {
+    PIDE.session.statistics -= main
+    PIDE.session.global_options -= main
+  }
 }
-

--- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Apr 15 11:47:29 2015 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Apr 15 13:55:01 2015 +0200
@@ -9,6 +9,8 @@
 
 import isabelle._
 
+import java.awt.BorderLayout
+
 import scala.swing.{TextArea, ScrollPane}
 
 import org.gjt.sp.jedit.View
@@ -16,21 +18,47 @@
 
 class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
 {
+  /* controls */
+
+  private val ml_stats = new Isabelle.ML_Stats
+
+  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats)
+
+
+  /* text area */
+
   private val text_area = new TextArea
+
+
+  /* layout */
+
   set_content(new ScrollPane(text_area))
+  add(controls.peer, BorderLayout.NORTH)
 
 
   /* main */
 
   private val main =
-    Session.Consumer[Prover.Message](getClass.getName) {
+    Session.Consumer[Any](getClass.getName) {
       case input: Prover.Input =>
         GUI_Thread.later { text_area.append(input.toString + "\n\n") }
 
       case output: Prover.Output =>
         GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
+
+      case _: Session.Global_Options =>
+        GUI_Thread.later { ml_stats.load() }
     }
 
-  override def init() { PIDE.session.all_messages += main }
-  override def exit() { PIDE.session.all_messages -= main }
+  override def init()
+  {
+    PIDE.session.all_messages += main
+    PIDE.session.global_options += main
+  }
+
+  override def exit()
+  {
+    PIDE.session.all_messages -= main
+    PIDE.session.global_options -= main
+  }
 }