tuned signature;
authorwenzelm
Wed Aug 05 16:13:42 2015 +0200 (2015-08-05)
changeset 608439980f3bcdea2
parent 60842 5510c8444bc4
child 60844 f7f2bc0e4293
tuned signature;
etc/options
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jedit_options.scala
     1.1 --- a/etc/options	Wed Aug 05 14:18:07 2015 +0200
     1.2 +++ b/etc/options	Wed Aug 05 16:13:42 2015 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    -- "ML debugger in single-step mode"
     1.5  
     1.6  public option ML_statistics : bool = true
     1.7 -  -- "ML runtime system statistics"
     1.8 +  -- "ML run-time system statistics"
     1.9  
    1.10  
    1.11  section "Editor Reactivity"
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Aug 05 14:18:07 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Aug 05 16:13:42 2015 +0200
     2.3 @@ -201,24 +201,8 @@
     2.4  
     2.5    /* ML statistics */
     2.6  
     2.7 -  private val ML_STATISTICS = "ML_statistics"
     2.8 -
     2.9 -  def ml_statistics: Boolean = PIDE.options.bool(ML_STATISTICS)
    2.10 -  def ml_statistics_=(b: Boolean): Unit =
    2.11 -    GUI_Thread.require {
    2.12 -      if (ml_statistics != b) {
    2.13 -        PIDE.options.bool(ML_STATISTICS) = b
    2.14 -        PIDE.session.update_options(PIDE.options.value)
    2.15 -      }
    2.16 -    }
    2.17 -
    2.18 -  class ML_Stats extends CheckBox("ML statistics")
    2.19 -  {
    2.20 -    tooltip = "Enable ML runtime system statistics"
    2.21 -    reactions += { case ButtonClicked(_) => ml_statistics = selected }
    2.22 -    def load() { selected = ml_statistics }
    2.23 -    load()
    2.24 -  }
    2.25 +  class ML_Stats extends
    2.26 +    JEdit_Options.Check_Box("ML_statistics", "ML statistics", "Enable ML runtime system statistics")
    2.27  
    2.28  
    2.29    /* required document nodes */
     3.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Wed Aug 05 14:18:07 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Aug 05 16:13:42 2015 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4  import javax.swing.text.JTextComponent
     3.5  
     3.6  import scala.swing.{Component, CheckBox, TextArea}
     3.7 +import scala.swing.event.ButtonClicked
     3.8  
     3.9  import org.gjt.sp.jedit.gui.ColorWellButton
    3.10  
    3.11 @@ -28,6 +29,23 @@
    3.12  object JEdit_Options
    3.13  {
    3.14    val RENDERING_SECTION = "Rendering of Document Content"
    3.15 +
    3.16 +  class Check_Box(name: String, label: String, description: String) extends CheckBox(label)
    3.17 +  {
    3.18 +    tooltip = description
    3.19 +    reactions += { case ButtonClicked(_) => update(selected) }
    3.20 +
    3.21 +    def stored: Boolean = PIDE.options.bool(name)
    3.22 +    def load() { selected = stored }
    3.23 +    def update(b: Boolean): Unit =
    3.24 +      GUI_Thread.require {
    3.25 +        if (selected != b) selected = b
    3.26 +        if (stored != b) {
    3.27 +          PIDE.options.bool(name) = b
    3.28 +          PIDE.session.update_options(PIDE.options.value)
    3.29 +        }
    3.30 +      }
    3.31 +  }
    3.32  }
    3.33  
    3.34  class JEdit_Options extends Options_Variable