1.1 --- a/doc-src/System/Thy/Sessions.thy	Sat Jul 28 18:20:47 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Sessions.thy	Sat Jul 28 19:37:35 2012 +0200
     1.3 @@ -115,14 +115,22 @@
     1.4    again.
     1.5  
     1.6    \end{description}
     1.7 +*}
     1.8  
     1.9 -  Plenty of examples may be found in the Isabelle distribution, such
    1.10 -  as in @{file "~~/src/HOL/ROOT"}.  *}
    1.11 +subsubsection {* Examples *}
    1.12 +
    1.13 +text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
    1.14 +  relevant situations. *}
    1.15  
    1.16  
    1.17  section {* System build options \label{sec:system-options} *}
    1.18  
    1.19 -text {* FIXME *}
    1.20 +text {* See @{file "~~/etc/options"} for the main defaults provided by
    1.21 +  the Isabelle distribution.
    1.22 +
    1.23 +  Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
    1.24 +  editing mode @{verbatim "isabelle-options"} for this file-format.
    1.25 +*}
    1.26  
    1.27  
    1.28  section {* Invoking the build process \label{sec:tool-build} *}

     2.1 --- a/etc/options	Sat Jul 28 18:20:47 2012 +0200
     2.2 +++ b/etc/options	Sat Jul 28 19:37:35 2012 +0200
     2.3 @@ -1,39 +1,63 @@
     2.4  (* :mode=isabelle-options: *)
     2.5  
     2.6  declare browser_info : bool = false
     2.7 +  -- "generate theory browser information"
     2.8  
     2.9  declare document : string = ""
    2.10 +  -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
    2.11  declare document_variants : string = "outline=/proof,/ML"
    2.12 +  -- "declare alternative document variants (separated by colons)"
    2.13  declare document_graph : bool = false
    2.14 +  -- "generate session graph image for document"
    2.15  declare document_dump : string = ""
    2.16 +  -- "dump generated document sources into given directory"
    2.17  declare document_dump_mode : string = "all"
    2.18 -declare no_document : bool = false
    2.19 +  -- "specific document dump mode: all, tex, tex+sty"
    2.20  
    2.21  declare threads : int = 0
    2.22 +  -- "maximum number of worker threads for prover process (0 = hardware max.)"
    2.23  declare threads_trace : int = 0
    2.24 +  -- "level of tracing information for multithreading"
    2.25  declare parallel_proofs : int = 2
    2.26 +  -- "level of parallel proof checking: 0, 1, 2"
    2.27  declare parallel_proofs_threshold : int = 100
    2.28 +  -- "threshold for sub-proof parallelization"
    2.29  
    2.30  declare print_mode : string = ""
    2.31 +  -- "additional print modes for prover output (separated by commas)"
    2.32  
    2.33  declare proofs : int = 1
    2.34 +  -- "level of detail for proof objects: 0, 1, 2"
    2.35  declare quick_and_dirty : bool = false
    2.36 +  -- "if true then some tools will OMIT some proofs"
    2.37  
    2.38  declare condition : string = ""
    2.39 +  -- "required environment variables for subsequent theories (separated by commas)"
    2.40  
    2.41  declare show_question_marks : bool = true
    2.42 +  -- "show leading question mark of schematic variables"
    2.43  
    2.44  declare names_long : bool = false
    2.45 +  -- "show fully qualified names"
    2.46  declare names_short : bool = false
    2.47 +  -- "show base names only"
    2.48  declare names_unique : bool = true
    2.49 +  -- "show partially qualified names, as required for unique name resolution"
    2.50  
    2.51  declare pretty_margin : int = 76
    2.52 +  -- "right margin / page width of pretty printer in Isabelle/ML"
    2.53  
    2.54  declare thy_output_display : bool = false
    2.55 +  -- "indicate output as multi-line display-style material"
    2.56 +declare thy_output_break : bool = false
    2.57 +  -- "control line breaks in non-display material"
    2.58  declare thy_output_quotes : bool = false
    2.59 +  -- "indicate if the output should be enclosed in double quotes"
    2.60  declare thy_output_indent : int = 0
    2.61 +  -- "indentation for pretty printing of display material"
    2.62  declare thy_output_source : bool = false
    2.63 -declare thy_output_break : bool = false
    2.64 +  -- "print original source text rather than internal representation"
    2.65  
    2.66  declare timing : bool = false
    2.67 +  -- "global timing of toplevel command execution and theory processing"
    2.68  

     3.1 --- a/src/Pure/System/options.scala	Sat Jul 28 18:20:47 2012 +0200
     3.2 +++ b/src/Pure/System/options.scala	Sat Jul 28 19:37:35 2012 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4      val DECLARE = "declare"
     3.5      val DEFINE = "define"
     3.6  
     3.7 -    val syntax = Outer_Syntax.empty + ":" + "=" + DECLARE + DEFINE
     3.8 +    val syntax = Outer_Syntax.empty + ":" + "=" + "--" + DECLARE + DEFINE
     3.9  
    3.10      val entry: Parser[Options => Options] =
    3.11      {
    3.12 @@ -44,9 +44,8 @@
    3.13        val option_value = atom("option value", tok => tok.is_name || tok.is_float)
    3.14  
    3.15        keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
    3.16 -      keyword("=") ~ option_value ~ opt(text)) ^^
    3.17 -        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) =>
    3.18 -            (options: Options) => options.declare(a, b, c, d.getOrElse("")) } |
    3.19 +      keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    3.20 +        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
    3.21        keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
    3.22          { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
    3.23      }