GUI controls for ML_statistics, for more digestible protocol dump;
authorwenzelm
Wed Apr 15 13:55:01 2015 +0200 (2015-04-15)
changeset 6007438a64cc17403
parent 60073 76a8400a58d9
child 60075 b079ee0e766c
GUI controls for ML_statistics, for more digestible protocol dump;
etc/options
src/Pure/PIDE/protocol.ML
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/protocol_dockable.scala
     1.1 --- a/etc/options	Wed Apr 15 11:47:29 2015 +0200
     1.2 +++ b/etc/options	Wed Apr 15 13:55:01 2015 +0200
     1.3 @@ -101,6 +101,9 @@
     1.4  public option ML_exception_trace : bool = false
     1.5    -- "ML exception trace for toplevel command execution"
     1.6  
     1.7 +public option ML_statistics : bool = true
     1.8 +  -- "ML runtime system statistics"
     1.9 +
    1.10  
    1.11  section "Editor Reactivity"
    1.12  
     2.1 --- a/src/Pure/PIDE/protocol.ML	Wed Apr 15 11:47:29 2015 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Apr 15 13:55:01 2015 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4      (fn [options_yxml] =>
     2.5        let val options = Options.decode (YXML.parse_body options_yxml) in
     2.6          Options.set_default options;
     2.7 -        Future.ML_statistics := true;
     2.8 +        Future.ML_statistics := Options.bool options "ML_statistics";
     2.9          Multithreading.trace := Options.int options "threads_trace";
    2.10          Multithreading.max_threads_update (Options.int options "threads");
    2.11          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Apr 15 11:47:29 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Apr 15 13:55:01 2015 +0200
     3.3 @@ -173,17 +173,14 @@
     3.4    private val CONTINUOUS_CHECKING = "editor_continuous_checking"
     3.5  
     3.6    def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
     3.7 -
     3.8 -  def continuous_checking_=(b: Boolean)
     3.9 -  {
    3.10 -    GUI_Thread.require {}
    3.11 -
    3.12 -    if (continuous_checking != b) {
    3.13 -      PIDE.options.bool(CONTINUOUS_CHECKING) = b
    3.14 -      PIDE.options_changed()
    3.15 -      PIDE.editor.flush()
    3.16 +  def continuous_checking_=(b: Boolean): Unit =
    3.17 +    GUI_Thread.require {
    3.18 +      if (continuous_checking != b) {
    3.19 +        PIDE.options.bool(CONTINUOUS_CHECKING) = b
    3.20 +        PIDE.options_changed()
    3.21 +        PIDE.editor.flush()
    3.22 +      }
    3.23      }
    3.24 -  }
    3.25  
    3.26    def set_continuous_checking() { continuous_checking = true }
    3.27    def reset_continuous_checking() { continuous_checking = false }
    3.28 @@ -198,6 +195,28 @@
    3.29    }
    3.30  
    3.31  
    3.32 +  /* ML statistics */
    3.33 +
    3.34 +  private val ML_STATISTICS = "ML_statistics"
    3.35 +
    3.36 +  def ml_statistics: Boolean = PIDE.options.bool(ML_STATISTICS)
    3.37 +  def ml_statistics_=(b: Boolean): Unit =
    3.38 +    GUI_Thread.require {
    3.39 +      if (ml_statistics != b) {
    3.40 +        PIDE.options.bool(ML_STATISTICS) = b
    3.41 +        PIDE.session.update_options(PIDE.options.value)
    3.42 +      }
    3.43 +    }
    3.44 +
    3.45 +  class ML_Stats extends CheckBox("ML statistics")
    3.46 +  {
    3.47 +    tooltip = "Enable ML runtime system statistics"
    3.48 +    reactions += { case ButtonClicked(_) => ml_statistics = selected }
    3.49 +    def load() { selected = ml_statistics }
    3.50 +    load()
    3.51 +  }
    3.52 +
    3.53 +
    3.54    /* required document nodes */
    3.55  
    3.56    private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
     4.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Apr 15 11:47:29 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed Apr 15 13:55:01 2015 +0200
     4.3 @@ -44,6 +44,8 @@
     4.4  
     4.5    /* controls */
     4.6  
     4.7 +  private val ml_stats = new Isabelle.ML_Stats
     4.8 +
     4.9    private val select_data = new ComboBox[String](
    4.10      ML_Statistics.standard_fields.map(_._1))
    4.11    {
    4.12 @@ -65,7 +67,8 @@
    4.13      }
    4.14    }
    4.15  
    4.16 -  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
    4.17 +  private val controls =
    4.18 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data)
    4.19  
    4.20  
    4.21    /* layout */
    4.22 @@ -77,13 +80,24 @@
    4.23    /* main */
    4.24  
    4.25    private val main =
    4.26 -    Session.Consumer[Session.Statistics](getClass.getName) {
    4.27 -      case stats =>
    4.28 +    Session.Consumer[Any](getClass.getName) {
    4.29 +      case stats: Session.Statistics =>
    4.30          rev_stats.change(stats.props :: _)
    4.31          delay_update.invoke()
    4.32 +
    4.33 +      case _: Session.Global_Options =>
    4.34 +        GUI_Thread.later { ml_stats.load() }
    4.35      }
    4.36  
    4.37 -  override def init() { PIDE.session.statistics += main }
    4.38 -  override def exit() { PIDE.session.statistics -= main }
    4.39 +  override def init()
    4.40 +  {
    4.41 +    PIDE.session.statistics += main
    4.42 +    PIDE.session.global_options += main
    4.43 +  }
    4.44 +
    4.45 +  override def exit()
    4.46 +  {
    4.47 +    PIDE.session.statistics -= main
    4.48 +    PIDE.session.global_options -= main
    4.49 +  }
    4.50  }
    4.51 -
     5.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Apr 15 11:47:29 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Apr 15 13:55:01 2015 +0200
     5.3 @@ -9,6 +9,8 @@
     5.4  
     5.5  import isabelle._
     5.6  
     5.7 +import java.awt.BorderLayout
     5.8 +
     5.9  import scala.swing.{TextArea, ScrollPane}
    5.10  
    5.11  import org.gjt.sp.jedit.View
    5.12 @@ -16,21 +18,47 @@
    5.13  
    5.14  class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
    5.15  {
    5.16 +  /* controls */
    5.17 +
    5.18 +  private val ml_stats = new Isabelle.ML_Stats
    5.19 +
    5.20 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats)
    5.21 +
    5.22 +
    5.23 +  /* text area */
    5.24 +
    5.25    private val text_area = new TextArea
    5.26 +
    5.27 +
    5.28 +  /* layout */
    5.29 +
    5.30    set_content(new ScrollPane(text_area))
    5.31 +  add(controls.peer, BorderLayout.NORTH)
    5.32  
    5.33  
    5.34    /* main */
    5.35  
    5.36    private val main =
    5.37 -    Session.Consumer[Prover.Message](getClass.getName) {
    5.38 +    Session.Consumer[Any](getClass.getName) {
    5.39        case input: Prover.Input =>
    5.40          GUI_Thread.later { text_area.append(input.toString + "\n\n") }
    5.41  
    5.42        case output: Prover.Output =>
    5.43          GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
    5.44 +
    5.45 +      case _: Session.Global_Options =>
    5.46 +        GUI_Thread.later { ml_stats.load() }
    5.47      }
    5.48  
    5.49 -  override def init() { PIDE.session.all_messages += main }
    5.50 -  override def exit() { PIDE.session.all_messages -= main }
    5.51 +  override def init()
    5.52 +  {
    5.53 +    PIDE.session.all_messages += main
    5.54 +    PIDE.session.global_options += main
    5.55 +  }
    5.56 +
    5.57 +  override def exit()
    5.58 +  {
    5.59 +    PIDE.session.all_messages -= main
    5.60 +    PIDE.session.global_options -= main
    5.61 +  }
    5.62  }