removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
--- 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) }
--- 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
}
}
--- 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
}
}