# HG changeset patch
# User wenzelm
# Date 1597224131 -7200
# Node ID f67e83608745e46c6e7c04ad272f3b9336239413
# Parent  f40200b5bb3cc97e953fe71aff51b90eb51347df
removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);

diff -r f40200b5bb3c -r f67e83608745 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Aug 12 11:07:14 2020 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Aug 12 11:22:11 2020 +0200
@@ -220,12 +220,6 @@
     state_dockable(view).foreach(_.update_request())
 
 
-  /* ML statistics */
-
-  class ML_Stats extends
-    JEdit_Options.Check_Box("ML_statistics", "ML statistics", "Enable ML runtime system statistics")
-
-
   /* required document nodes */
 
   def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) }
diff -r f40200b5bb3c -r f67e83608745 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Aug 12 11:07:14 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed Aug 12 11:22:11 2020 +0200
@@ -67,8 +67,6 @@
 
   /* controls */
 
-  private val ml_stats = new Isabelle.ML_Stats
-
   private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1))
   {
     tooltip = "Select visualized data collection"
@@ -95,7 +93,7 @@
     reactions += { case ValueChanged(_) => input_delay.invoke() }
   }
 
-  private val controls = Wrap_Panel(List(ml_stats, select_data, reset_data, limit_data))
+  private val controls = Wrap_Panel(List(select_data, reset_data, limit_data))
 
 
   /* layout */
@@ -107,24 +105,19 @@
   /* main */
 
   private val main =
-    Session.Consumer[Any](getClass.getName) {
-      case stats: Session.Runtime_Statistics =>
+    Session.Consumer[Session.Runtime_Statistics](getClass.getName) {
+      case stats =>
         add_statistics(stats.props)
         update_delay.invoke()
-
-      case _: Session.Global_Options =>
-        GUI_Thread.later { ml_stats.load() }
     }
 
   override def init()
   {
     PIDE.session.runtime_statistics += main
-    PIDE.session.global_options += main
   }
 
   override def exit()
   {
     PIDE.session.runtime_statistics -= main
-    PIDE.session.global_options -= main
   }
 }
diff -r f40200b5bb3c -r f67e83608745 src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Aug 12 11:07:14 2020 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Aug 12 11:22:11 2020 +0200
@@ -19,13 +19,6 @@
 
 class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  /* controls */
-
-  private val ml_stats = new Isabelle.ML_Stats
-
-  private val controls = Wrap_Panel(List(ml_stats))
-
-
   /* text area */
 
   private val text_area = new TextArea
@@ -34,32 +27,26 @@
   /* layout */
 
   set_content(new ScrollPane(text_area))
-  add(controls.peer, BorderLayout.NORTH)
 
 
   /* main */
 
   private val main =
-    Session.Consumer[Any](getClass.getName) {
+    Session.Consumer[Prover.Message](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
-    PIDE.session.global_options += main
   }
 
   override def exit()
   {
     PIDE.session.all_messages -= main
-    PIDE.session.global_options -= main
   }
 }