--- a/etc/options Tue Jul 24 00:29:36 2012 +0200
+++ b/etc/options Tue Jul 24 10:11:49 2012 +0200
@@ -2,11 +2,11 @@
declare browser_info : bool = false
-declare document : bool = true
-declare document_format : string = pdf
+declare document : string = ""
declare document_variants : string = document
declare document_graph : bool = false
declare document_dump : string = ""
+declare no_document : bool = false
declare threads_limit : int = 1
declare threads_trace : int = 0
--- a/src/FOL/ROOT Tue Jul 24 00:29:36 2012 +0200
+++ b/src/FOL/ROOT Tue Jul 24 10:11:49 2012 +0200
@@ -21,6 +21,6 @@
Quantifiers_Cla
Miniscope
If
- theories [document = false] "Locale_Test/Locale_Test"
+ theories [no_document] "Locale_Test/Locale_Test"
files "document/root.tex"
--- a/src/HOL/ROOT Tue Jul 24 00:29:36 2012 +0200
+++ b/src/HOL/ROOT Tue Jul 24 10:11:49 2012 +0200
@@ -6,22 +6,22 @@
session "HOL-Base"! in "." = Pure +
description {* Raw HOL base, with minimal tools *}
- options [document = false]
+ options [no_document]
theories HOL
session "HOL-Plain"! in "." = Pure +
description {* HOL side-entry after bootstrap of many tools and packages *}
- options [document = false]
+ options [no_document]
theories Plain
session "HOL-Main"! in "." = Pure +
description {* HOL side-entry for Main only, without Complex_Main *}
- options [document = false]
+ options [no_document]
theories Main
session "HOL-Proofs"! (2) in "." = Pure +
description {* HOL-Main with proof terms *}
- options [document = false, proofs = 2, parallel_proofs = 0]
+ options [no_document, proofs = 2, parallel_proofs = 0]
theories Main
session HOLCF! (3) = HOL +
@@ -32,7 +32,7 @@
HOLCF -- a semantic extension of HOL by the LCF logic.
*}
options [document_graph]
- theories [document = false]
+ theories [no_document]
"~~/src/HOL/Library/Nat_Bijection"
"~~/src/HOL/Library/Countable"
theories Plain_HOLCF Fixrec HOLCF
--- a/src/Pure/System/build.ML Tue Jul 24 00:29:36 2012 +0200
+++ b/src/Pure/System/build.ML Tue Jul 24 10:11:49 2012 +0200
@@ -22,7 +22,8 @@
|> Unsynchronized.setmp Goal.parallel_proofs_threshold
(Options.int options "parallel_proofs_threshold")
|> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
- |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit");
+ |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit")
+ |> Options.bool options "no_document" ? Present.no_document;
fun build args_file =
let
@@ -38,7 +39,7 @@
save
false (* FIXME reset!? *)
(Options.bool options "browser_info") browser_info
- (Options.string options "document_format") (* FIXME dependent on "document" (!?) *)
+ (Options.string options "document")
(Options.bool options "document_graph")
(space_explode "," (Options.string options "document_variants"))
parent