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) }