clarified format of etc/options: only declarations, not re-definitions;
authorwenzelm
Tue Aug 14 13:01:09 2012 +0200 (2012-08-14)
changeset 48795bece259ee055
parent 48794 8d2a026e576b
child 48804 6348e5fca42e
clarified format of etc/options: only declarations, not re-definitions;
etc/options
src/Pure/System/options.scala
     1.1 --- a/etc/options	Tue Aug 14 12:26:02 2012 +0200
     1.2 +++ b/etc/options	Tue Aug 14 13:01:09 2012 +0200
     1.3 @@ -1,68 +1,68 @@
     1.4  (* :mode=isabelle-options: *)
     1.5  
     1.6 -declare browser_info : bool = false
     1.7 +option browser_info : bool = false
     1.8    -- "generate theory browser information"
     1.9  
    1.10 -declare document : string = ""
    1.11 +option document : string = ""
    1.12    -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
    1.13 -declare document_variants : string = "outline=/proof,/ML"
    1.14 -  -- "declare alternative document variants (separated by colons)"
    1.15 -declare document_graph : bool = false
    1.16 +option document_variants : string = "outline=/proof,/ML"
    1.17 +  -- "option alternative document variants (separated by colons)"
    1.18 +option document_graph : bool = false
    1.19    -- "generate session graph image for document"
    1.20 -declare document_dump : string = ""
    1.21 +option document_dump : string = ""
    1.22    -- "dump generated document sources into given directory"
    1.23 -declare document_dump_mode : string = "all"
    1.24 +option document_dump_mode : string = "all"
    1.25    -- "specific document dump mode: all, tex, tex+sty"
    1.26  
    1.27 -declare threads : int = 0
    1.28 +option threads : int = 0
    1.29    -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.30 -declare threads_trace : int = 0
    1.31 +option threads_trace : int = 0
    1.32    -- "level of tracing information for multithreading"
    1.33 -declare parallel_proofs : int = 2
    1.34 +option parallel_proofs : int = 2
    1.35    -- "level of parallel proof checking: 0, 1, 2"
    1.36 -declare parallel_proofs_threshold : int = 100
    1.37 +option parallel_proofs_threshold : int = 100
    1.38    -- "threshold for sub-proof parallelization"
    1.39  
    1.40 -declare print_mode : string = ""
    1.41 +option print_mode : string = ""
    1.42    -- "additional print modes for prover output (separated by commas)"
    1.43  
    1.44 -declare proofs : int = 1
    1.45 +option proofs : int = 1
    1.46    -- "level of detail for proof objects: 0, 1, 2"
    1.47 -declare quick_and_dirty : bool = false
    1.48 +option quick_and_dirty : bool = false
    1.49    -- "if true then some tools will OMIT some proofs"
    1.50 -declare skip_proofs : bool = false
    1.51 +option skip_proofs : bool = false
    1.52    -- "skip over proofs"
    1.53  
    1.54 -declare condition : string = ""
    1.55 +option condition : string = ""
    1.56    -- "required environment variables for subsequent theories (separated by commas)"
    1.57  
    1.58 -declare show_question_marks : bool = true
    1.59 +option show_question_marks : bool = true
    1.60    -- "show leading question mark of schematic variables"
    1.61  
    1.62 -declare names_long : bool = false
    1.63 +option names_long : bool = false
    1.64    -- "show fully qualified names"
    1.65 -declare names_short : bool = false
    1.66 +option names_short : bool = false
    1.67    -- "show base names only"
    1.68 -declare names_unique : bool = true
    1.69 +option names_unique : bool = true
    1.70    -- "show partially qualified names, as required for unique name resolution"
    1.71  
    1.72 -declare pretty_margin : int = 76
    1.73 +option pretty_margin : int = 76
    1.74    -- "right margin / page width of pretty printer in Isabelle/ML"
    1.75  
    1.76 -declare thy_output_display : bool = false
    1.77 +option thy_output_display : bool = false
    1.78    -- "indicate output as multi-line display-style material"
    1.79 -declare thy_output_break : bool = false
    1.80 +option thy_output_break : bool = false
    1.81    -- "control line breaks in non-display material"
    1.82 -declare thy_output_quotes : bool = false
    1.83 +option thy_output_quotes : bool = false
    1.84    -- "indicate if the output should be enclosed in double quotes"
    1.85 -declare thy_output_indent : int = 0
    1.86 +option thy_output_indent : int = 0
    1.87    -- "indentation for pretty printing of display material"
    1.88 -declare thy_output_source : bool = false
    1.89 +option thy_output_source : bool = false
    1.90    -- "print original source text rather than internal representation"
    1.91  
    1.92 -declare timing : bool = false
    1.93 +option timing : bool = false
    1.94    -- "global timing of toplevel command execution and theory processing"
    1.95  
    1.96 -declare timeout : real = 0
    1.97 +option timeout : real = 0
    1.98    -- "timeout for session build job (seconds > 0)"
    1.99  
     2.1 --- a/src/Pure/System/options.scala	Tue Aug 14 12:26:02 2012 +0200
     2.2 +++ b/src/Pure/System/options.scala	Tue Aug 14 13:01:09 2012 +0200
     2.3 @@ -30,12 +30,10 @@
     2.4  
     2.5    /* parsing */
     2.6  
     2.7 -  private val DECLARE = "declare"
     2.8 -  private val DEFINE = "define"
     2.9 +  private val OPTION = "option"
    2.10  
    2.11    lazy val options_syntax =
    2.12 -    Outer_Syntax.init() + ":" + "=" + "--" +
    2.13 -      (DECLARE, Keyword.THY_DECL) + (DEFINE, Keyword.PRF_DECL)
    2.14 +    Outer_Syntax.init() + ":" + "=" + "--" + (OPTION, Keyword.THY_DECL)
    2.15  
    2.16    private object Parser extends Parse.Parser
    2.17    {
    2.18 @@ -49,11 +47,9 @@
    2.19            { case s ~ n => if (s.isDefined) "-" + n else n } |
    2.20          atom("option value", tok => tok.is_name || tok.is_float)
    2.21  
    2.22 -      command(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
    2.23 +      command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
    2.24        keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    2.25 -        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
    2.26 -      command(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
    2.27 -        { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
    2.28 +        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
    2.29      }
    2.30  
    2.31      def parse_entries(file: Path): List[Options => Options] =
    2.32 @@ -114,7 +110,7 @@
    2.33  
    2.34    def print: String =
    2.35      cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
    2.36 -      name + " : " + opt.typ.print + " = " +
    2.37 +      "option " + name + " : " + opt.typ.print + " = " +
    2.38          (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
    2.39        "\n  -- " + quote(opt.description) }))
    2.40