# HG changeset patch
# User wenzelm
# Date 1343117509 -7200
# Node ID 09710d6fc3d1ecbdafd5e45e0d364e67c192290c
# Parent  fd9e28d5a14352b79f732a6701242e14d1e8acbb
clarified document options;

diff -r fd9e28d5a143 -r 09710d6fc3d1 etc/options
--- 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
diff -r fd9e28d5a143 -r 09710d6fc3d1 src/FOL/ROOT
--- 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"
 
diff -r fd9e28d5a143 -r 09710d6fc3d1 src/HOL/ROOT
--- 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
diff -r fd9e28d5a143 -r 09710d6fc3d1 src/Pure/System/build.ML
--- 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