src/Tools/jEdit/src/isabelle.scala
changeset 72135 f67e83608745
parent 71601 97ccf48c2f0c
child 72927 69f768aff611
--- 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) }