# HG changeset patch # User wenzelm # Date 1429098901 -7200 # Node ID 38a64cc17403b825b1bee7bdd89acba47bc28e97 # Parent 76a8400a58d9ed57192612c5a4e62f039ffec125 GUI controls for ML_statistics, for more digestible protocol dump; diff -r 76a8400a58d9 -r 38a64cc17403 etc/options --- 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" diff -r 76a8400a58d9 -r 38a64cc17403 src/Pure/PIDE/protocol.ML --- 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) diff -r 76a8400a58d9 -r 38a64cc17403 src/Tools/jEdit/src/isabelle.scala --- 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) diff -r 76a8400a58d9 -r 38a64cc17403 src/Tools/jEdit/src/monitor_dockable.scala --- 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 + } } - diff -r 76a8400a58d9 -r 38a64cc17403 src/Tools/jEdit/src/protocol_dockable.scala --- 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 + } }