# HG changeset patch
# User wenzelm
# Date 1368873691 -7200
# Node ID 78f2475aa1267439f069bb9d8bf4168a2ce6f9b4
# Parent  4b4ff1d3b723a62a04aaf2eae06b28d8febc8851
explicit notion of public options, which are shown in the editor options dialog;
avoid hard-wired stuff;

diff -r 4b4ff1d3b723 -r 78f2475aa126 etc/options
--- a/etc/options	Fri May 17 23:31:02 2013 +0200
+++ b/etc/options	Sat May 18 12:41:31 2013 +0200
@@ -65,15 +65,15 @@
 
 section "Parallel Checking"
 
-option threads : int = 0
+public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
-option threads_trace : int = 0
+public option threads_trace : int = 0
   -- "level of tracing information for multithreading"
-option parallel_proofs : int = 2
+public option parallel_proofs : int = 2
   -- "level of parallel proof checking: 0, 1, 2"
-option parallel_subproofs_saturation : int = 100
+public option parallel_subproofs_saturation : int = 100
   -- "upper bound for forks of nested proofs (multiplied by worker threads)"
-option parallel_subproofs_threshold : real = 0.01
+public option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
 
@@ -104,26 +104,26 @@
 
 section "Editor Reactivity"
 
-option editor_skip_proofs : bool = false
+public option editor_skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
 
-option editor_load_delay : real = 0.5
+public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
-option editor_input_delay : real = 0.3
+public option editor_input_delay : real = 0.3
   -- "delay for user input (text edits, cursor movement etc.)"
 
-option editor_output_delay : real = 0.1
+public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
-option editor_update_delay : real = 0.5
+public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
-option editor_reparse_limit : int = 10000
+public option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
-option editor_tracing_messages : int = 1000
+public option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction"
 
-option editor_chart_delay : real = 3.0
+public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
diff -r 4b4ff1d3b723 -r 78f2475aa126 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri May 17 23:31:02 2013 +0200
+++ b/src/Pure/System/options.scala	Sat May 18 12:41:31 2013 +0200
@@ -29,7 +29,7 @@
   case object String extends Type
   case object Unknown extends Type
 
-  case class Opt(name: String, typ: Type, value: String, default_value: String,
+  case class Opt(public: Boolean, name: String, typ: Type, value: String, default_value: String,
     description: String, section: String)
   {
     private def print(default: Boolean): String =
@@ -61,6 +61,7 @@
   /* parsing */
 
   private val SECTION = "section"
+  private val PUBLIC = "public"
   private val OPTION = "option"
   private val OPTIONS = Path.explode("etc/options")
   private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
@@ -69,7 +70,7 @@
 
   lazy val options_syntax =
     Outer_Syntax.init() + ":" + "=" + "--" +
-      (SECTION, Keyword.THY_HEADING2) + (OPTION, Keyword.THY_DECL)
+      (SECTION, Keyword.THY_HEADING2) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
 
   lazy val prefs_syntax = Outer_Syntax.init() + "="
 
@@ -86,9 +87,10 @@
     {
       command(SECTION) ~! text ^^
         { case _ ~ a => (options: Options) => options.set_section(a) } |
-      command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
+      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
-        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
+        { case a ~ _ ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+            (options: Options) => options.declare(a.isDefined, b, c, d, e) }
     }
 
     val prefs_entry: Parser[Options => Options] =
@@ -250,7 +252,8 @@
     }
   }
 
-  def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
+  def declare(public: Boolean, name: String, typ_name: String, value: String, description: String)
+    : Options =
   {
     options.get(name) match {
       case Some(_) => error("Duplicate declaration of option " + quote(name))
@@ -263,7 +266,7 @@
             case "string" => Options.String
             case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
           }
-        val opt = Options.Opt(name, typ, value, value, description, section)
+        val opt = Options.Opt(public, name, typ, value, value, description, section)
         (new Options(options + (name -> opt), section)).check_value(name)
     }
   }
@@ -273,7 +276,8 @@
     if (options.isDefinedAt(name)) this + (name, value)
     else
       new Options(
-        options + (name -> Options.Opt(name, Options.Unknown, value, value, "", "")), section)
+        options +
+          (name -> Options.Opt(false, name, Options.Unknown, value, value, "", "")), section)
   }
 
   def + (name: String, value: String): Options =
diff -r 4b4ff1d3b723 -r 78f2475aa126 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Fri May 17 23:31:02 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Sat May 18 12:41:31 2013 +0200
@@ -1,33 +1,33 @@
 (* :mode=isabelle-options: *)
 
-option jedit_logic : string = ""
+public option jedit_logic : string = ""
   -- "default logic session"
 
-option jedit_font_scale : real = 1.0
+public option jedit_font_scale : real = 1.0
   -- "scale factor of add-on panels wrt. main text area"
 
-option jedit_tooltip_delay : real = 0.75
+public option jedit_tooltip_delay : real = 0.75
   -- "open/close delay for document tooltips"
 
-option jedit_tooltip_font_scale : real = 0.85
+public option jedit_tooltip_font_scale : real = 0.85
   -- "scale factor of tooltips wrt. main text area"
 
-option jedit_tooltip_margin : int = 60
+public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-option jedit_tooltip_bounds : real = 0.5
+public option jedit_tooltip_bounds : real = 0.5
   -- "relative bounds of tooltip window wrt. logical screen size"
 
-option jedit_text_overview_limit : int = 100000
+public option jedit_text_overview_limit : int = 100000
   -- "maximum amount of text to visualize in overview column"
 
-option jedit_symbols_search_limit : int = 50
+public option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"
 
-option jedit_mac_adapter : bool = true
+public option jedit_mac_adapter : bool = true
   -- "some native Mac OS X support (potential conflict with MacOSX plugin)"
 
-option jedit_timing_threshold : real = 0.1
+public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display"
 
 
diff -r 4b4ff1d3b723 -r 78f2475aa126 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri May 17 23:31:02 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat May 18 12:41:31 2013 +0200
@@ -39,30 +39,19 @@
 
 class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
 {
-  // FIXME avoid hard-wired stuff
-  private val relevant_options =
-    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
-      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
-      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
-      "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs",
-      "parallel_subproofs_saturation", "editor_skip_proofs", "editor_load_delay",
-      "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
-      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
-
-  relevant_options.foreach(PIDE.options.value.check_name _)
-
+  val options = PIDE.options
   protected val components =
-    PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
+    options.make_components(List(Isabelle_Logic.logic_selector(false)),
+      (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
 }
 
 
 class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
 {
-  // FIXME avoid hard-wired stuff
   private val predefined =
     (for {
       (name, opt) <- PIDE.options.value.options.toList
-      if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
+      if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
     } yield PIDE.options.make_color_component(opt))
 
   assert(!predefined.isEmpty)
diff -r 4b4ff1d3b723 -r 78f2475aa126 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri May 17 23:31:02 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat May 18 12:41:31 2013 +0200
@@ -25,6 +25,11 @@
   def save(): Unit
 }
 
+object JEdit_Options
+{
+  val RENDERING_SECTION = "Rendering of Document Content"
+}
+
 class JEdit_Options extends Options_Variable
 {
   def color_value(s: String): Color = Color_Value(string(s))