some support to organize options in sections;
authorwenzelm
Tue Sep 11 15:47:42 2012 +0200 (2012-09-11)
changeset 49270e5d162d15867
parent 49269 7157af98ca55
child 49271 b08f9d534a2a
some support to organize options in sections;
etc/options
src/Pure/System/options.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/jedit_options.scala
     1.1 --- a/etc/options	Tue Sep 11 11:53:34 2012 +0200
     1.2 +++ b/etc/options	Tue Sep 11 15:47:42 2012 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (* :mode=isabelle-options: *)
     1.5  
     1.6 +section {* Document preparation *}
     1.7 +
     1.8  option browser_info : bool = false
     1.9    -- "generate theory browser information"
    1.10  
    1.11 @@ -16,28 +18,6 @@
    1.12  option document_dump_mode : string = "all"
    1.13    -- "specific document dump mode: all, tex, tex+sty"
    1.14  
    1.15 -option threads : int = 0
    1.16 -  -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.17 -option threads_trace : int = 0
    1.18 -  -- "level of tracing information for multithreading"
    1.19 -option parallel_proofs : int = 2
    1.20 -  -- "level of parallel proof checking: 0, 1, 2"
    1.21 -option parallel_proofs_threshold : int = 100
    1.22 -  -- "threshold for sub-proof parallelization"
    1.23 -
    1.24 -option print_mode : string = ""
    1.25 -  -- "additional print modes for prover output (separated by commas)"
    1.26 -
    1.27 -option proofs : int = 1
    1.28 -  -- "level of detail for proof objects: 0, 1, 2"
    1.29 -option quick_and_dirty : bool = false
    1.30 -  -- "if true then some tools will OMIT some proofs"
    1.31 -option skip_proofs : bool = false
    1.32 -  -- "skip over proofs"
    1.33 -
    1.34 -option condition : string = ""
    1.35 -  -- "required environment variables for subsequent theories (separated by commas)"
    1.36 -
    1.37  option show_question_marks : bool = true
    1.38    -- "show leading question mark of schematic variables"
    1.39  
    1.40 @@ -62,6 +42,38 @@
    1.41  option thy_output_source : bool = false
    1.42    -- "print original source text rather than internal representation"
    1.43  
    1.44 +
    1.45 +option print_mode : string = ""
    1.46 +  -- "additional print modes for prover output (separated by commas)"
    1.47 +
    1.48 +
    1.49 +section {* Parallel checking *}
    1.50 +
    1.51 +option threads : int = 0
    1.52 +  -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.53 +option threads_trace : int = 0
    1.54 +  -- "level of tracing information for multithreading"
    1.55 +option parallel_proofs : int = 2
    1.56 +  -- "level of parallel proof checking: 0, 1, 2"
    1.57 +option parallel_proofs_threshold : int = 100
    1.58 +  -- "threshold for sub-proof parallelization"
    1.59 +
    1.60 +
    1.61 +section {* Detail of proof recording *}
    1.62 +
    1.63 +option proofs : int = 1
    1.64 +  -- "level of detail for proof objects: 0, 1, 2"
    1.65 +option quick_and_dirty : bool = false
    1.66 +  -- "if true then some tools will OMIT some proofs"
    1.67 +option skip_proofs : bool = false
    1.68 +  -- "skip over proofs"
    1.69 +
    1.70 +
    1.71 +section {* Global session parameters *}
    1.72 +
    1.73 +option condition : string = ""
    1.74 +  -- "required environment variables for subsequent theories (separated by commas)"
    1.75 +
    1.76  option timing : bool = false
    1.77    -- "global timing of toplevel command execution and theory processing"
    1.78  
     2.1 --- a/src/Pure/System/options.scala	Tue Sep 11 11:53:34 2012 +0200
     2.2 +++ b/src/Pure/System/options.scala	Tue Sep 11 15:47:42 2012 +0200
     2.3 @@ -30,25 +30,40 @@
     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, description: String)
     2.8 +  case class Opt(name: String, typ: Type, value: String, description: String, section: String)
     2.9    {
    2.10      def print: String =
    2.11        "option " + name + " : " + typ.print + " = " +
    2.12          (if (typ == Options.String) quote(value) else value) +
    2.13        (if (description == "") "" else "\n  -- " + quote(description))
    2.14  
    2.15 +    def title(strip: String): String =
    2.16 +    {
    2.17 +      val words = space_explode('_', name)
    2.18 +      val words1 =
    2.19 +        words match {
    2.20 +          case word :: rest if word == strip => rest
    2.21 +          case _ => words
    2.22 +        }
    2.23 +      words1.map(Library.capitalize).mkString(" ")
    2.24 +    }
    2.25 +
    2.26      def unknown: Boolean = typ == Unknown
    2.27    }
    2.28  
    2.29  
    2.30    /* parsing */
    2.31  
    2.32 +  private val SECTION = "section"
    2.33    private val OPTION = "option"
    2.34    private val OPTIONS = Path.explode("etc/options")
    2.35    private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
    2.36    private val PREFS_BACKUP = Path.explode("$ISABELLE_HOME_USER/etc/preferences~")
    2.37  
    2.38 -  lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + (OPTION, Keyword.THY_DECL)
    2.39 +  lazy val options_syntax =
    2.40 +    Outer_Syntax.init() + ":" + "=" + "--" +
    2.41 +      (SECTION, Keyword.THY_HEADING2) + (OPTION, Keyword.THY_DECL)
    2.42 +
    2.43    lazy val prefs_syntax = Outer_Syntax.init() + "="
    2.44  
    2.45    object Parser extends Parse.Parser
    2.46 @@ -62,6 +77,8 @@
    2.47  
    2.48      val option_entry: Parser[Options => Options] =
    2.49      {
    2.50 +      command(SECTION) ~! text ^^
    2.51 +        { case _ ~ a => (options: Options) => options.set_section(a.trim) } |
    2.52        command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
    2.53        keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    2.54          { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
    2.55 @@ -82,7 +99,7 @@
    2.56            case Success(result, _) => result
    2.57            case bad => error(bad.toString)
    2.58          }
    2.59 -      try { (options /: ops) { case (opts, op) => op(opts) } }
    2.60 +      try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
    2.61        catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
    2.62      }
    2.63    }
    2.64 @@ -125,24 +142,14 @@
    2.65  }
    2.66  
    2.67  
    2.68 -final class Options private(protected val options: Map[String, Options.Opt] = Map.empty)
    2.69 +final class Options private(
    2.70 +  protected val options: Map[String, Options.Opt] = Map.empty,
    2.71 +  val section: String = "")
    2.72  {
    2.73    override def toString: String = options.iterator.mkString("Options (", ",", ")")
    2.74  
    2.75    def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
    2.76  
    2.77 -  def title(strip: String, name: String): String =
    2.78 -  {
    2.79 -    check_name(name)
    2.80 -    val words = space_explode('_', name)
    2.81 -    val words1 =
    2.82 -      words match {
    2.83 -        case word :: rest if word == strip => rest
    2.84 -        case _ => words
    2.85 -      }
    2.86 -    words1.map(Library.capitalize).mkString(" ")
    2.87 -  }
    2.88 -
    2.89    def description(name: String): String = check_name(name).description
    2.90  
    2.91  
    2.92 @@ -167,7 +174,7 @@
    2.93    private def put[A](name: String, typ: Options.Type, value: String): Options =
    2.94    {
    2.95      val opt = check_type(name, typ)
    2.96 -    new Options(options + (name -> opt.copy(value = value)))
    2.97 +    new Options(options + (name -> opt.copy(value = value)), section)
    2.98    }
    2.99  
   2.100    private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
   2.101 @@ -239,21 +246,21 @@
   2.102              case "string" => Options.String
   2.103              case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
   2.104            }
   2.105 -        val opt = Options.Opt(name, typ, value, description)
   2.106 -        (new Options(options + (name -> opt))).check_value(name)
   2.107 +        val opt = Options.Opt(name, typ, value, description, section)
   2.108 +        (new Options(options + (name -> opt), section)).check_value(name)
   2.109      }
   2.110    }
   2.111  
   2.112    def add_permissive(name: String, value: String): Options =
   2.113    {
   2.114      if (options.isDefinedAt(name)) this + (name, value)
   2.115 -    else new Options(options + (name -> Options.Opt(name, Options.Unknown, value, "")))
   2.116 +    else new Options(options + (name -> Options.Opt(name, Options.Unknown, value, "", "")), section)
   2.117    }
   2.118  
   2.119    def + (name: String, value: String): Options =
   2.120    {
   2.121      val opt = check_name(name)
   2.122 -    (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
   2.123 +    (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
   2.124    }
   2.125  
   2.126    def + (name: String, opt_value: Option[String]): Options =
   2.127 @@ -278,6 +285,15 @@
   2.128      (this /: specs)({ case (x, (y, z)) => x + (y, z) })
   2.129  
   2.130  
   2.131 +  /* sections */
   2.132 +
   2.133 +  def set_section(new_section: String): Options =
   2.134 +    new Options(options, new_section)
   2.135 +
   2.136 +  def sections: List[(String, List[Options.Opt])] =
   2.137 +    options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) })
   2.138 +
   2.139 +
   2.140    /* encode */
   2.141  
   2.142    def encode: XML.Body =
     3.1 --- a/src/Tools/jEdit/etc/options	Tue Sep 11 11:53:34 2012 +0200
     3.2 +++ b/src/Tools/jEdit/etc/options	Tue Sep 11 15:47:42 2012 +0200
     3.3 @@ -18,5 +18,8 @@
     3.4  option jedit_tooltip_dismiss_delay : real = 8.0
     3.5    -- "global delay for Swing tooltips"
     3.6  
     3.7 +
     3.8 +section {* Reactivity *}
     3.9 +
    3.10  option jedit_load_delay : real = 0.5
    3.11    -- "delay for file load operations (new buffers etc.)"
     4.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Sep 11 11:53:34 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Sep 11 15:47:42 2012 +0200
     4.3 @@ -27,6 +27,8 @@
     4.4      override def toString = description
     4.5    }
     4.6  
     4.7 +  private val opt_name = "jedit_logic"
     4.8 +
     4.9    def logic_selector(autosave: Boolean): Option_Component =
    4.10    {
    4.11      Swing_Thread.require()
    4.12 @@ -36,16 +38,17 @@
    4.13          Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
    4.14  
    4.15      val component = new ComboBox(entries) with Option_Component {
    4.16 -      val title = Isabelle.options.title("jedit_logic")
    4.17 +      name = opt_name
    4.18 +      val title = "Logic"
    4.19        def load: Unit =
    4.20        {
    4.21 -        val logic = Isabelle.options.string("jedit_logic")
    4.22 +        val logic = Isabelle.options.string(opt_name)
    4.23          entries.find(_.name == logic) match {
    4.24            case Some(entry) => selection.item = entry
    4.25            case None =>
    4.26          }
    4.27        }
    4.28 -      def save: Unit = Isabelle.options.string("jedit_logic") = selection.item.name
    4.29 +      def save: Unit = Isabelle.options.string(opt_name) = selection.item.name
    4.30      }
    4.31  
    4.32      component.load()
    4.33 @@ -53,7 +56,7 @@
    4.34        component.listenTo(component.selection)
    4.35        component.reactions += { case SelectionChanged(_) => component.save() }
    4.36      }
    4.37 -    component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print)
    4.38 +    component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name(opt_name).print)
    4.39      component
    4.40    }
    4.41  
    4.42 @@ -61,7 +64,7 @@
    4.43    {
    4.44      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
    4.45      val logic =
    4.46 -      Isabelle.options.string("jedit_logic") match {
    4.47 +      Isabelle.options.string(opt_name) match {
    4.48          case "" => default_logic()
    4.49          case logic => logic
    4.50        }
     5.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 11:53:34 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 15:47:42 2012 +0200
     5.3 @@ -14,22 +14,24 @@
     5.4  
     5.5  class Isabelle_Options extends AbstractOptionPane("isabelle")
     5.6  {
     5.7 -  private val components = List(
     5.8 -    Isabelle_Logic.logic_selector(false),
     5.9 -    Isabelle.options.make_component("jedit_auto_start"),
    5.10 -    Isabelle.options.make_component("jedit_relative_font_size"),
    5.11 -    Isabelle.options.make_component("jedit_tooltip_font_size"),
    5.12 -    Isabelle.options.make_component("jedit_tooltip_margin"),
    5.13 -    Isabelle.options.make_component("jedit_tooltip_dismiss_delay"),
    5.14 -    Isabelle.options.make_component("jedit_load_delay"))
    5.15 +  // FIXME avoid hard-wired stuff
    5.16 +  private val relevant_options =
    5.17 +    Set("jedit_logic", "jedit_auto_start", "jedit_relative_font_size", "jedit_tooltip_font_size",
    5.18 +      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay")
    5.19 +
    5.20 +  private val components =
    5.21 +    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
    5.22  
    5.23    override def _init()
    5.24    {
    5.25 -    for (c <- components) addComponent(c.title, c.peer)
    5.26 +    for ((s, cs) <- components) {
    5.27 +      if (s == "") addSeparator() else addSeparator(s)
    5.28 +      cs.foreach(c => addComponent(c.title, c.peer))
    5.29 +    }
    5.30    }
    5.31  
    5.32    override def _save()
    5.33    {
    5.34 -    for (c <- components) c.save()
    5.35 +    for ((_, cs) <- components) cs.foreach(_.save())
    5.36    }
    5.37  }
     6.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 11:53:34 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 15:47:42 2012 +0200
     6.3 @@ -24,18 +24,17 @@
     6.4  
     6.5  class JEdit_Options extends Options_Variable
     6.6  {
     6.7 -  def title(opt_name: String): String = value.title("jedit", opt_name)
     6.8 -
     6.9 -  def make_component(opt_name: String): Option_Component =
    6.10 +  def make_component(opt: Options.Opt): Option_Component =
    6.11    {
    6.12      Swing_Thread.require()
    6.13  
    6.14 -    val opt = value.check_name(opt_name)
    6.15 -    val opt_title = title(opt_name)
    6.16 +    val opt_name = opt.name
    6.17 +    val opt_title = opt.title("jedit")
    6.18  
    6.19      val component =
    6.20        if (opt.typ == Options.Bool)
    6.21          new CheckBox with Option_Component {
    6.22 +          name = opt_name
    6.23            val title = opt_title
    6.24            def load = selected = bool(opt_name)
    6.25            def save = bool(opt_name) = selected
    6.26 @@ -45,6 +44,7 @@
    6.27          val text_area =
    6.28            new TextArea with Option_Component {
    6.29              if (default_font != null) font = default_font
    6.30 +            name = opt_name
    6.31              val title = opt_title
    6.32              def load = text = value.check_name(opt_name).value
    6.33              def save = update(value + (opt_name, text))
    6.34 @@ -64,5 +64,18 @@
    6.35      component.tooltip = Isabelle.tooltip(opt.print)
    6.36      component
    6.37    }
    6.38 +
    6.39 +  def make_components(predefined: List[Option_Component], filter: String => Boolean)
    6.40 +    : List[(String, List[Option_Component])] =
    6.41 +  {
    6.42 +    def mk_component(opt: Options.Opt): List[Option_Component] =
    6.43 +      predefined.find(opt.name == _.name) match {
    6.44 +        case Some(c) => List(c)
    6.45 +        case None => if (filter(opt.name)) List(make_component(opt)) else Nil
    6.46 +      }
    6.47 +    value.sections.sortBy(_._1).map(
    6.48 +        { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component _)) })
    6.49 +      .filterNot(_._2.isEmpty)
    6.50 +  }
    6.51  }
    6.52