# HG changeset patch
# User wenzelm
# Date 1347385512 -7200
# Node ID 66058a677ddd38c9e758c2c708962a2c27b6df4c
# Parent  ebe2a5cec4bf031a205c5ddbef9131ee1a49b08b# Parent  64bed36cd8da8d31761f8d9dea7da65314d50832
merged

diff -r ebe2a5cec4bf -r 66058a677ddd etc/options
--- a/etc/options	Tue Sep 11 18:58:29 2012 +0200
+++ b/etc/options	Tue Sep 11 19:45:12 2012 +0200
@@ -1,5 +1,7 @@
 (* :mode=isabelle-options: *)
 
+section {* Document preparation *}
+
 option browser_info : bool = false
   -- "generate theory browser information"
 
@@ -16,28 +18,6 @@
 option document_dump_mode : string = "all"
   -- "specific document dump mode: all, tex, tex+sty"
 
-option threads : int = 0
-  -- "maximum number of worker threads for prover process (0 = hardware max.)"
-option threads_trace : int = 0
-  -- "level of tracing information for multithreading"
-option parallel_proofs : int = 2
-  -- "level of parallel proof checking: 0, 1, 2"
-option parallel_proofs_threshold : int = 100
-  -- "threshold for sub-proof parallelization"
-
-option print_mode : string = ""
-  -- "additional print modes for prover output (separated by commas)"
-
-option proofs : int = 1
-  -- "level of detail for proof objects: 0, 1, 2"
-option quick_and_dirty : bool = false
-  -- "if true then some tools will OMIT some proofs"
-option skip_proofs : bool = false
-  -- "skip over proofs"
-
-option condition : string = ""
-  -- "required environment variables for subsequent theories (separated by commas)"
-
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 
@@ -62,9 +42,56 @@
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
 
+
+option print_mode : string = ""
+  -- "additional print modes for prover output (separated by commas)"
+
+
+section {* Parallel checking *}
+
+option threads : int = 0
+  -- "maximum number of worker threads for prover process (0 = hardware max.)"
+option threads_trace : int = 0
+  -- "level of tracing information for multithreading"
+option parallel_proofs : int = 2
+  -- "level of parallel proof checking: 0, 1, 2"
+option parallel_proofs_threshold : int = 100
+  -- "threshold for sub-proof parallelization"
+
+
+section {* Detail of proof recording *}
+
+option proofs : int = 1
+  -- "level of detail for proof objects: 0, 1, 2"
+option quick_and_dirty : bool = false
+  -- "if true then some tools will OMIT some proofs"
+option skip_proofs : bool = false
+  -- "skip over proofs"
+
+
+section {* Global session parameters *}
+
+option condition : string = ""
+  -- "required environment variables for subsequent theories (separated by commas)"
+
 option timing : bool = false
   -- "global timing of toplevel command execution and theory processing"
 
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
+
+section {* Editor reactivity *}
+
+option editor_load_delay : real = 0.5
+  -- "delay for file load operations (new buffers etc.)"
+
+option editor_input_delay : real = 0.3
+  -- "delay for user input (text edits, cursor movement etc.)"
+
+option editor_output_delay : real = 0.1
+  -- "delay for prover output (markup, common messages etc.)"
+
+option editor_update_delay : real = 0.5
+  -- "delay for physical GUI updates"
+
diff -r ebe2a5cec4bf -r 66058a677ddd src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -30,12 +30,30 @@
   case object String extends Type
   case object Unknown extends Type
 
-  case class Opt(name: String, typ: Type, value: String, description: String)
+  case class Opt(name: String, typ: Type, value: String, default_value: String,
+    description: String, section: String)
   {
-    def print: String =
+    private def print(default: Boolean): String =
+    {
+      val x = if (default) default_value else value
       "option " + name + " : " + typ.print + " = " +
-        (if (typ == Options.String) quote(value) else value) +
-      (if (description == "") "" else "\n  -- " + quote(description))
+        (if (typ == Options.String) quote(x) else x) +
+        (if (description == "") "" else "\n  -- " + quote(description))
+    }
+
+    def print: String = print(false)
+    def print_default: String = print(true)
+
+    def title(strip: String): String =
+    {
+      val words = space_explode('_', name)
+      val words1 =
+        words match {
+          case word :: rest if word == strip => rest
+          case _ => words
+        }
+      words1.map(Library.capitalize).mkString(" ")
+    }
 
     def unknown: Boolean = typ == Unknown
   }
@@ -43,12 +61,16 @@
 
   /* parsing */
 
+  private val SECTION = "section"
   private val OPTION = "option"
   private val OPTIONS = Path.explode("etc/options")
   private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
   private val PREFS_BACKUP = Path.explode("$ISABELLE_HOME_USER/etc/preferences~")
 
-  lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + (OPTION, Keyword.THY_DECL)
+  lazy val options_syntax =
+    Outer_Syntax.init() + ":" + "=" + "--" +
+      (SECTION, Keyword.THY_HEADING2) + (OPTION, Keyword.THY_DECL)
+
   lazy val prefs_syntax = Outer_Syntax.init() + "="
 
   object Parser extends Parse.Parser
@@ -62,6 +84,8 @@
 
     val option_entry: Parser[Options => Options] =
     {
+      command(SECTION) ~! text ^^
+        { case _ ~ a => (options: Options) => options.set_section(a.trim) } |
       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) }
@@ -82,7 +106,7 @@
           case Success(result, _) => result
           case bad => error(bad.toString)
         }
-      try { (options /: ops) { case (opts, op) => op(opts) } }
+      try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
       catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
     }
   }
@@ -125,24 +149,14 @@
 }
 
 
-final class Options private(protected val options: Map[String, Options.Opt] = Map.empty)
+final class Options private(
+  protected val options: Map[String, Options.Opt] = Map.empty,
+  val section: String = "")
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")
 
   def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
 
-  def title(strip: String, name: String): String =
-  {
-    check_name(name)
-    val words = space_explode('_', name)
-    val words1 =
-      words match {
-        case word :: rest if word == strip => rest
-        case _ => words
-      }
-    words1.map(Library.capitalize).mkString(" ")
-  }
-
   def description(name: String): String = check_name(name).description
 
 
@@ -167,7 +181,7 @@
   private def put[A](name: String, typ: Options.Type, value: String): Options =
   {
     val opt = check_type(name, typ)
-    new Options(options + (name -> opt.copy(value = value)))
+    new Options(options + (name -> opt.copy(value = value)), section)
   }
 
   private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
@@ -239,21 +253,23 @@
             case "string" => Options.String
             case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
           }
-        val opt = Options.Opt(name, typ, value, description)
-        (new Options(options + (name -> opt))).check_value(name)
+        val opt = Options.Opt(name, typ, value, value, description, section)
+        (new Options(options + (name -> opt), section)).check_value(name)
     }
   }
 
   def add_permissive(name: String, value: String): Options =
   {
     if (options.isDefinedAt(name)) this + (name, value)
-    else new Options(options + (name -> Options.Opt(name, Options.Unknown, value, "")))
+    else
+      new Options(
+        options + (name -> Options.Opt(name, Options.Unknown, value, value, "", "")), section)
   }
 
   def + (name: String, value: String): Options =
   {
     val opt = check_name(name)
-    (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
+    (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
   }
 
   def + (name: String, opt_value: Option[String]): Options =
@@ -278,6 +294,15 @@
     (this /: specs)({ case (x, (y, z)) => x + (y, z) })
 
 
+  /* sections */
+
+  def set_section(new_section: String): Options =
+    new Options(options, new_section)
+
+  def sections: List[(String, List[Options.Opt])] =
+    options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) })
+
+
   /* encode */
 
   def encode: XML.Body =
diff -r ebe2a5cec4bf -r 66058a677ddd src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -46,15 +46,14 @@
   @volatile var verbose: Boolean = false
 
 
-  /* tuning parameters */  // FIXME properties or settings (!?)
+  /* tuning parameters */
+
+  def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
 
-  val message_delay = Time.seconds(0.01)  // prover messages
-  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
-  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
-  val update_delay = Time.seconds(0.5)  // GUI layout updates
-  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
-  val prune_size = 0  // size of retained history
-  val syslog_limit = 100
+  private val message_delay = Time.seconds(0.01)  // incoming prover messages
+  private val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
+  private val prune_size = 0  // size of retained history
+  private val syslog_limit = 100
 
 
   /* pervasive event buses */
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 19:45:12 2012 +0200
@@ -6,8 +6,8 @@
 option jedit_auto_start : bool = true
   -- "auto-start prover session on editor startup"
 
-option jedit_relative_font_size : int = 100
-  -- "relative font size of output panel wrt. main text area"
+option jedit_font_scale : real = 1.0
+  -- "scale factor of add-on panels wrt. main text area"
 
 option jedit_tooltip_font_size : int = 10
   -- "tooltip font size (according to HTML)"
@@ -17,6 +17,3 @@
 
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
-
-option jedit_load_delay : real = 0.5
-  -- "delay for file load operations (new buffers etc.)"
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -115,7 +115,8 @@
     }
 
     private val delay_flush =
-      Swing_Thread.delay_last(session.input_delay) { flush() }
+      Swing_Thread.delay_last(
+        Time.seconds(Isabelle.options.real("editor_input_delay"))) { flush() }
 
     def +=(edit: Text.Edit)
     {
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -341,7 +341,7 @@
   }
 
   private val delay_caret_update =
-    Swing_Thread.delay_last(session.input_delay) {
+    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
       session.caret_focus.event(Session.Caret_Focus)
     }
 
@@ -355,7 +355,8 @@
   private object overview extends Text_Overview(this)
   {
     val delay_repaint =
-      Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
+      Swing_Thread.delay_first(
+        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
   }
 
 
@@ -366,7 +367,8 @@
       react {
         case _: Session.Raw_Edits =>
           Swing_Thread.later {
-            overview.delay_repaint.postpone(Isabelle.session.input_delay)
+            overview.delay_repaint.postpone(
+              Time.seconds(Isabelle.options.real("editor_input_delay")))
           }
 
         case changed: Session.Commands_Changed =>
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -27,6 +27,8 @@
     override def toString = description
   }
 
+  private val opt_name = "jedit_logic"
+
   def logic_selector(autosave: Boolean): Option_Component =
   {
     Swing_Thread.require()
@@ -36,16 +38,17 @@
         Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
 
     val component = new ComboBox(entries) with Option_Component {
-      val title = Isabelle.options.title("jedit_logic")
+      name = opt_name
+      val title = "Logic"
       def load: Unit =
       {
-        val logic = Isabelle.options.string("jedit_logic")
+        val logic = Isabelle.options.string(opt_name)
         entries.find(_.name == logic) match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
-      def save: Unit = Isabelle.options.string("jedit_logic") = selection.item.name
+      def save: Unit = Isabelle.options.string(opt_name) = selection.item.name
     }
 
     component.load()
@@ -53,7 +56,7 @@
       component.listenTo(component.selection)
       component.reactions += { case SelectionChanged(_) => component.save() }
     }
-    component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print)
+    component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name(opt_name).print_default)
     component
   }
 
@@ -61,7 +64,7 @@
   {
     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     val logic =
-      Isabelle.options.string("jedit_logic") match {
+      Isabelle.options.string(opt_name) match {
         case "" => default_logic()
         case logic => logic
       }
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -9,27 +9,38 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.AbstractOptionPane
+import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
 
 
 class Isabelle_Options extends AbstractOptionPane("isabelle")
 {
-  private val components = List(
-    Isabelle_Logic.logic_selector(false),
-    Isabelle.options.make_component("jedit_auto_start"),
-    Isabelle.options.make_component("jedit_relative_font_size"),
-    Isabelle.options.make_component("jedit_tooltip_font_size"),
-    Isabelle.options.make_component("jedit_tooltip_margin"),
-    Isabelle.options.make_component("jedit_tooltip_dismiss_delay"),
-    Isabelle.options.make_component("jedit_load_delay"))
+  // FIXME avoid hard-wired stuff
+  private val relevant_options =
+    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
+      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
+      "editor_input_delay", "editor_output_delay", "editor_update_delay")
+
+  relevant_options.foreach(Isabelle.options.value.check_name _)
+
+  private val components =
+    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
 
   override def _init()
   {
-    for (c <- components) addComponent(c.title, c.peer)
+    val dummy_property = "options.isabelle.dummy"
+
+    for ((s, cs) <- components) {
+      if (s != "") {
+        jEdit.setProperty(dummy_property, s)
+        addSeparator(dummy_property)
+        jEdit.setProperty(dummy_property, null)
+      }
+      cs.foreach(c => addComponent(c.title, c.peer))
+    }
   }
 
   override def _save()
   {
-    for (c <- components) c.save()
+    for ((_, cs) <- components) cs.foreach(_.save())
   }
 }
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -24,18 +24,17 @@
 
 class JEdit_Options extends Options_Variable
 {
-  def title(opt_name: String): String = value.title("jedit", opt_name)
-
-  def make_component(opt_name: String): Option_Component =
+  def make_component(opt: Options.Opt): Option_Component =
   {
     Swing_Thread.require()
 
-    val opt = value.check_name(opt_name)
-    val opt_title = title(opt_name)
+    val opt_name = opt.name
+    val opt_title = opt.title("jedit")
 
     val component =
       if (opt.typ == Options.Bool)
         new CheckBox with Option_Component {
+          name = opt_name
           val title = opt_title
           def load = selected = bool(opt_name)
           def save = bool(opt_name) = selected
@@ -45,6 +44,7 @@
         val text_area =
           new TextArea with Option_Component {
             if (default_font != null) font = default_font
+            name = opt_name
             val title = opt_title
             def load = text = value.check_name(opt_name).value
             def save = update(value + (opt_name, text))
@@ -61,8 +61,21 @@
         text_area
       }
     component.load()
-    component.tooltip = Isabelle.tooltip(opt.print)
+    component.tooltip = Isabelle.tooltip(opt.print_default)
     component
   }
+
+  def make_components(predefined: List[Option_Component], filter: String => Boolean)
+    : List[(String, List[Option_Component])] =
+  {
+    def mk_component(opt: Options.Opt): List[Option_Component] =
+      predefined.find(opt.name == _.name) match {
+        case Some(c) => List(c)
+        case None => if (filter(opt.name)) List(make_component(opt)) else Nil
+      }
+    value.sections.sortBy(_._1).map(
+        { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component _)) })
+      .filterNot(_._2.isEmpty)
+  }
 }
 
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -148,7 +148,8 @@
   /* resize */
 
   private val delay_resize =
-    Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
+    Swing_Thread.delay_first(
+      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r ebe2a5cec4bf -r 66058a677ddd src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 18:58:29 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 19:45:12 2012 +0200
@@ -58,8 +58,7 @@
   def font_family(): String = jEdit.getProperty("view.font")
 
   def font_size(): Float =
-    (jEdit.getIntegerProperty("view.fontsize", 16) *
-      options.int("jedit_relative_font_size")).toFloat / 100
+    (jEdit.getIntegerProperty("view.fontsize", 16) * options.real("jedit_font_scale")).toFloat
 
 
   /* tooltip markup */
@@ -261,7 +260,7 @@
   /* theory files */
 
   private lazy val delay_load =
-    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("jedit_load_delay")))
+    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_load_delay")))
     {
       val view = jEdit.getActiveView()
 
@@ -407,7 +406,9 @@
 
       val content = Isabelle_Logic.session_content(false)
       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
-      Isabelle.session = new Session(thy_load)
+      Isabelle.session = new Session(thy_load) {
+        override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
+      }
 
       Isabelle.session.phase_changed += session_manager
       Isabelle.startup_failure = None