explicit notion of public options, which are shown in the editor options dialog;
authorwenzelm
Sat May 18 12:41:31 2013 +0200 (2013-05-18)
changeset 5206578f2475aa126
parent 52064 4b4ff1d3b723
child 52066 83b7b88770c9
explicit notion of public options, which are shown in the editor options dialog;
avoid hard-wired stuff;
etc/options
src/Pure/System/options.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/jedit_options.scala
     1.1 --- a/etc/options	Fri May 17 23:31:02 2013 +0200
     1.2 +++ b/etc/options	Sat May 18 12:41:31 2013 +0200
     1.3 @@ -65,15 +65,15 @@
     1.4  
     1.5  section "Parallel Checking"
     1.6  
     1.7 -option threads : int = 0
     1.8 +public option threads : int = 0
     1.9    -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.10 -option threads_trace : int = 0
    1.11 +public option threads_trace : int = 0
    1.12    -- "level of tracing information for multithreading"
    1.13 -option parallel_proofs : int = 2
    1.14 +public option parallel_proofs : int = 2
    1.15    -- "level of parallel proof checking: 0, 1, 2"
    1.16 -option parallel_subproofs_saturation : int = 100
    1.17 +public option parallel_subproofs_saturation : int = 100
    1.18    -- "upper bound for forks of nested proofs (multiplied by worker threads)"
    1.19 -option parallel_subproofs_threshold : real = 0.01
    1.20 +public option parallel_subproofs_threshold : real = 0.01
    1.21    -- "lower bound of timing estimate for forked nested proofs (seconds)"
    1.22  
    1.23  
    1.24 @@ -104,26 +104,26 @@
    1.25  
    1.26  section "Editor Reactivity"
    1.27  
    1.28 -option editor_skip_proofs : bool = false
    1.29 +public option editor_skip_proofs : bool = false
    1.30    -- "skip over proofs (implicit 'sorry')"
    1.31  
    1.32 -option editor_load_delay : real = 0.5
    1.33 +public option editor_load_delay : real = 0.5
    1.34    -- "delay for file load operations (new buffers etc.)"
    1.35  
    1.36 -option editor_input_delay : real = 0.3
    1.37 +public option editor_input_delay : real = 0.3
    1.38    -- "delay for user input (text edits, cursor movement etc.)"
    1.39  
    1.40 -option editor_output_delay : real = 0.1
    1.41 +public option editor_output_delay : real = 0.1
    1.42    -- "delay for prover output (markup, common messages etc.)"
    1.43  
    1.44 -option editor_update_delay : real = 0.5
    1.45 +public option editor_update_delay : real = 0.5
    1.46    -- "delay for physical GUI updates"
    1.47  
    1.48 -option editor_reparse_limit : int = 10000
    1.49 +public option editor_reparse_limit : int = 10000
    1.50    -- "maximum amount of reparsed text outside perspective"
    1.51  
    1.52 -option editor_tracing_messages : int = 1000
    1.53 +public option editor_tracing_messages : int = 1000
    1.54    -- "initial number of tracing messages for each command transaction"
    1.55  
    1.56 -option editor_chart_delay : real = 3.0
    1.57 +public option editor_chart_delay : real = 3.0
    1.58    -- "delay for chart repainting"
     2.1 --- a/src/Pure/System/options.scala	Fri May 17 23:31:02 2013 +0200
     2.2 +++ b/src/Pure/System/options.scala	Sat May 18 12:41:31 2013 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4    case object String extends Type
     2.5    case object Unknown extends Type
     2.6  
     2.7 -  case class Opt(name: String, typ: Type, value: String, default_value: String,
     2.8 +  case class Opt(public: Boolean, name: String, typ: Type, value: String, default_value: String,
     2.9      description: String, section: String)
    2.10    {
    2.11      private def print(default: Boolean): String =
    2.12 @@ -61,6 +61,7 @@
    2.13    /* parsing */
    2.14  
    2.15    private val SECTION = "section"
    2.16 +  private val PUBLIC = "public"
    2.17    private val OPTION = "option"
    2.18    private val OPTIONS = Path.explode("etc/options")
    2.19    private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
    2.20 @@ -69,7 +70,7 @@
    2.21  
    2.22    lazy val options_syntax =
    2.23      Outer_Syntax.init() + ":" + "=" + "--" +
    2.24 -      (SECTION, Keyword.THY_HEADING2) + (OPTION, Keyword.THY_DECL)
    2.25 +      (SECTION, Keyword.THY_HEADING2) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
    2.26  
    2.27    lazy val prefs_syntax = Outer_Syntax.init() + "="
    2.28  
    2.29 @@ -86,9 +87,10 @@
    2.30      {
    2.31        command(SECTION) ~! text ^^
    2.32          { case _ ~ a => (options: Options) => options.set_section(a) } |
    2.33 -      command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
    2.34 +      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
    2.35        keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    2.36 -        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
    2.37 +        { case a ~ _ ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
    2.38 +            (options: Options) => options.declare(a.isDefined, b, c, d, e) }
    2.39      }
    2.40  
    2.41      val prefs_entry: Parser[Options => Options] =
    2.42 @@ -250,7 +252,8 @@
    2.43      }
    2.44    }
    2.45  
    2.46 -  def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
    2.47 +  def declare(public: Boolean, name: String, typ_name: String, value: String, description: String)
    2.48 +    : Options =
    2.49    {
    2.50      options.get(name) match {
    2.51        case Some(_) => error("Duplicate declaration of option " + quote(name))
    2.52 @@ -263,7 +266,7 @@
    2.53              case "string" => Options.String
    2.54              case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
    2.55            }
    2.56 -        val opt = Options.Opt(name, typ, value, value, description, section)
    2.57 +        val opt = Options.Opt(public, name, typ, value, value, description, section)
    2.58          (new Options(options + (name -> opt), section)).check_value(name)
    2.59      }
    2.60    }
    2.61 @@ -273,7 +276,8 @@
    2.62      if (options.isDefinedAt(name)) this + (name, value)
    2.63      else
    2.64        new Options(
    2.65 -        options + (name -> Options.Opt(name, Options.Unknown, value, value, "", "")), section)
    2.66 +        options +
    2.67 +          (name -> Options.Opt(false, name, Options.Unknown, value, value, "", "")), section)
    2.68    }
    2.69  
    2.70    def + (name: String, value: String): Options =
     3.1 --- a/src/Tools/jEdit/etc/options	Fri May 17 23:31:02 2013 +0200
     3.2 +++ b/src/Tools/jEdit/etc/options	Sat May 18 12:41:31 2013 +0200
     3.3 @@ -1,33 +1,33 @@
     3.4  (* :mode=isabelle-options: *)
     3.5  
     3.6 -option jedit_logic : string = ""
     3.7 +public option jedit_logic : string = ""
     3.8    -- "default logic session"
     3.9  
    3.10 -option jedit_font_scale : real = 1.0
    3.11 +public option jedit_font_scale : real = 1.0
    3.12    -- "scale factor of add-on panels wrt. main text area"
    3.13  
    3.14 -option jedit_tooltip_delay : real = 0.75
    3.15 +public option jedit_tooltip_delay : real = 0.75
    3.16    -- "open/close delay for document tooltips"
    3.17  
    3.18 -option jedit_tooltip_font_scale : real = 0.85
    3.19 +public option jedit_tooltip_font_scale : real = 0.85
    3.20    -- "scale factor of tooltips wrt. main text area"
    3.21  
    3.22 -option jedit_tooltip_margin : int = 60
    3.23 +public option jedit_tooltip_margin : int = 60
    3.24    -- "margin for tooltip pretty-printing"
    3.25  
    3.26 -option jedit_tooltip_bounds : real = 0.5
    3.27 +public option jedit_tooltip_bounds : real = 0.5
    3.28    -- "relative bounds of tooltip window wrt. logical screen size"
    3.29  
    3.30 -option jedit_text_overview_limit : int = 100000
    3.31 +public option jedit_text_overview_limit : int = 100000
    3.32    -- "maximum amount of text to visualize in overview column"
    3.33  
    3.34 -option jedit_symbols_search_limit : int = 50
    3.35 +public option jedit_symbols_search_limit : int = 50
    3.36    -- "maximum number of symbols in search result"
    3.37  
    3.38 -option jedit_mac_adapter : bool = true
    3.39 +public option jedit_mac_adapter : bool = true
    3.40    -- "some native Mac OS X support (potential conflict with MacOSX plugin)"
    3.41  
    3.42 -option jedit_timing_threshold : real = 0.1
    3.43 +public option jedit_timing_threshold : real = 0.1
    3.44    -- "default threshold for timing display"
    3.45  
    3.46  
     4.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Fri May 17 23:31:02 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat May 18 12:41:31 2013 +0200
     4.3 @@ -39,30 +39,19 @@
     4.4  
     4.5  class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
     4.6  {
     4.7 -  // FIXME avoid hard-wired stuff
     4.8 -  private val relevant_options =
     4.9 -    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
    4.10 -      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
    4.11 -      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
    4.12 -      "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs",
    4.13 -      "parallel_subproofs_saturation", "editor_skip_proofs", "editor_load_delay",
    4.14 -      "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
    4.15 -      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
    4.16 -
    4.17 -  relevant_options.foreach(PIDE.options.value.check_name _)
    4.18 -
    4.19 +  val options = PIDE.options
    4.20    protected val components =
    4.21 -    PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
    4.22 +    options.make_components(List(Isabelle_Logic.logic_selector(false)),
    4.23 +      (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
    4.24  }
    4.25  
    4.26  
    4.27  class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
    4.28  {
    4.29 -  // FIXME avoid hard-wired stuff
    4.30    private val predefined =
    4.31      (for {
    4.32        (name, opt) <- PIDE.options.value.options.toList
    4.33 -      if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
    4.34 +      if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
    4.35      } yield PIDE.options.make_color_component(opt))
    4.36  
    4.37    assert(!predefined.isEmpty)
     5.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Fri May 17 23:31:02 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Sat May 18 12:41:31 2013 +0200
     5.3 @@ -25,6 +25,11 @@
     5.4    def save(): Unit
     5.5  }
     5.6  
     5.7 +object JEdit_Options
     5.8 +{
     5.9 +  val RENDERING_SECTION = "Rendering of Document Content"
    5.10 +}
    5.11 +
    5.12  class JEdit_Options extends Options_Variable
    5.13  {
    5.14    def color_value(s: String): Color = Color_Value(string(s))