clarified document options;
authorwenzelm
Tue Jul 24 10:11:49 2012 +0200 (2012-07-24)
changeset 4845809710d6fc3d1
parent 48457 fd9e28d5a143
child 48459 375e45df6fdf
clarified document options;
etc/options
src/FOL/ROOT
src/HOL/ROOT
src/Pure/System/build.ML
     1.1 --- a/etc/options	Tue Jul 24 00:29:36 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 10:11:49 2012 +0200
     1.3 @@ -2,11 +2,11 @@
     1.4  
     1.5  declare browser_info : bool = false
     1.6  
     1.7 -declare document : bool = true
     1.8 -declare document_format : string = pdf
     1.9 +declare document : string = ""
    1.10  declare document_variants : string = document
    1.11  declare document_graph : bool = false
    1.12  declare document_dump : string = ""
    1.13 +declare no_document : bool = false
    1.14  
    1.15  declare threads_limit : int = 1
    1.16  declare threads_trace : int = 0
     2.1 --- a/src/FOL/ROOT	Tue Jul 24 00:29:36 2012 +0200
     2.2 +++ b/src/FOL/ROOT	Tue Jul 24 10:11:49 2012 +0200
     2.3 @@ -21,6 +21,6 @@
     2.4      Quantifiers_Cla
     2.5      Miniscope
     2.6      If
     2.7 -  theories [document = false] "Locale_Test/Locale_Test"
     2.8 +  theories [no_document] "Locale_Test/Locale_Test"
     2.9    files "document/root.tex"
    2.10  
     3.1 --- a/src/HOL/ROOT	Tue Jul 24 00:29:36 2012 +0200
     3.2 +++ b/src/HOL/ROOT	Tue Jul 24 10:11:49 2012 +0200
     3.3 @@ -6,22 +6,22 @@
     3.4  
     3.5  session "HOL-Base"! in "." = Pure +
     3.6    description {* Raw HOL base, with minimal tools *}
     3.7 -  options [document = false]
     3.8 +  options [no_document]
     3.9    theories HOL
    3.10  
    3.11  session "HOL-Plain"! in "." = Pure +
    3.12    description {* HOL side-entry after bootstrap of many tools and packages *}
    3.13 -  options [document = false]
    3.14 +  options [no_document]
    3.15    theories Plain
    3.16  
    3.17  session "HOL-Main"! in "." = Pure +
    3.18    description {* HOL side-entry for Main only, without Complex_Main *}
    3.19 -  options [document = false]
    3.20 +  options [no_document]
    3.21    theories Main
    3.22  
    3.23  session "HOL-Proofs"! (2) in "." = Pure +
    3.24    description {* HOL-Main with proof terms *}
    3.25 -  options [document = false, proofs = 2, parallel_proofs = 0]
    3.26 +  options [no_document, proofs = 2, parallel_proofs = 0]
    3.27    theories Main
    3.28  
    3.29  session HOLCF! (3) = HOL +
    3.30 @@ -32,7 +32,7 @@
    3.31      HOLCF -- a semantic extension of HOL by the LCF logic.
    3.32    *}
    3.33    options [document_graph]
    3.34 -  theories [document = false]
    3.35 +  theories [no_document]
    3.36      "~~/src/HOL/Library/Nat_Bijection"
    3.37      "~~/src/HOL/Library/Countable"
    3.38    theories Plain_HOLCF Fixrec HOLCF
     4.1 --- a/src/Pure/System/build.ML	Tue Jul 24 00:29:36 2012 +0200
     4.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 10:11:49 2012 +0200
     4.3 @@ -22,7 +22,8 @@
     4.4      |> Unsynchronized.setmp Goal.parallel_proofs_threshold
     4.5          (Options.int options "parallel_proofs_threshold")
     4.6      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     4.7 -    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit");
     4.8 +    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit")
     4.9 +    |> Options.bool options "no_document" ? Present.no_document;
    4.10  
    4.11  fun build args_file =
    4.12    let
    4.13 @@ -38,7 +39,7 @@
    4.14          save
    4.15          false (* FIXME reset!? *)
    4.16          (Options.bool options "browser_info") browser_info
    4.17 -        (Options.string options "document_format")   (* FIXME dependent on "document" (!?) *)
    4.18 +        (Options.string options "document")
    4.19          (Options.bool options "document_graph")
    4.20          (space_explode "," (Options.string options "document_variants"))
    4.21          parent