--- a/etc/options Tue Sep 11 11:53:34 2012 +0200
+++ b/etc/options Tue Sep 11 15:47:42 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,6 +42,38 @@
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"
--- a/src/Pure/System/options.scala Tue Sep 11 11:53:34 2012 +0200
+++ b/src/Pure/System/options.scala Tue Sep 11 15:47:42 2012 +0200
@@ -30,25 +30,40 @@
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, description: String, section: String)
{
def print: String =
"option " + name + " : " + typ.print + " = " +
(if (typ == Options.String) quote(value) else value) +
(if (description == "") "" else "\n -- " + quote(description))
+ 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
}
/* 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 +77,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 +99,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 +142,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 +174,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 +246,21 @@
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, 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, "", "")), 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 +285,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 =
--- a/src/Tools/jEdit/etc/options Tue Sep 11 11:53:34 2012 +0200
+++ b/src/Tools/jEdit/etc/options Tue Sep 11 15:47:42 2012 +0200
@@ -18,5 +18,8 @@
option jedit_tooltip_dismiss_delay : real = 8.0
-- "global delay for Swing tooltips"
+
+section {* Reactivity *}
+
option jedit_load_delay : real = 0.5
-- "delay for file load operations (new buffers etc.)"
--- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Sep 11 11:53:34 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Sep 11 15:47:42 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)
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
}
--- a/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 11:53:34 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 15:47:42 2012 +0200
@@ -14,22 +14,24 @@
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_relative_font_size", "jedit_tooltip_font_size",
+ "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay")
+
+ 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)
+ for ((s, cs) <- components) {
+ if (s == "") addSeparator() else addSeparator(s)
+ cs.foreach(c => addComponent(c.title, c.peer))
+ }
}
override def _save()
{
- for (c <- components) c.save()
+ for ((_, cs) <- components) cs.foreach(_.save())
}
}
--- a/src/Tools/jEdit/src/jedit_options.scala Tue Sep 11 11:53:34 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Tue Sep 11 15:47:42 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))
@@ -64,5 +64,18 @@
component.tooltip = Isabelle.tooltip(opt.print)
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)
+ }
}