# HG changeset patch
# User wenzelm
# Date 1343126313 -7200
# Node ID 7483aa690b4f387289d6e0cd19d97906db00f39a
# Parent  826a771cff339193df876d936a8c4d4545cbbbca
clarified "document" again, eliminated redundant "no_document";

diff -r 826a771cff33 -r 7483aa690b4f src/FOL/ROOT
--- a/src/FOL/ROOT	Tue Jul 24 12:28:20 2012 +0200
+++ b/src/FOL/ROOT	Tue Jul 24 12:38:33 2012 +0200
@@ -21,6 +21,6 @@
     Quantifiers_Cla
     Miniscope
     If
-  theories [no_document] "Locale_Test/Locale_Test"
+  theories [document = false] "Locale_Test/Locale_Test"
   files "document/root.tex"
 
diff -r 826a771cff33 -r 7483aa690b4f src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 24 12:28:20 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 24 12:38:33 2012 +0200
@@ -6,22 +6,22 @@
 
 session "HOL-Base"! in "." = Pure +
   description {* Raw HOL base, with minimal tools *}
-  options [no_document]
+  options [document = false]
   theories HOL
 
 session "HOL-Plain"! in "." = Pure +
   description {* HOL side-entry after bootstrap of many tools and packages *}
-  options [no_document]
+  options [document = false]
   theories Plain
 
 session "HOL-Main"! in "." = Pure +
   description {* HOL side-entry for Main only, without Complex_Main *}
-  options [no_document]
+  options [document = false]
   theories Main
 
 session "HOL-Proofs"! (2) in "." = Pure +
   description {* HOL-Main with proof terms *}
-  options [no_document, proofs = 2, parallel_proofs = 0]
+  options [document = false, 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 [no_document]
+  theories [document = false]
     "~~/src/HOL/Library/Nat_Bijection"
     "~~/src/HOL/Library/Countable"
   theories Plain_HOLCF Fixrec HOLCF
diff -r 826a771cff33 -r 7483aa690b4f src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 12:28:20 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 12:38:33 2012 +0200
@@ -24,7 +24,8 @@
         (Options.int options "parallel_proofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
-    |> Options.bool options "no_document" ? Present.no_document
+    |> (case Options.string options "document" of "" => false | "false" => false | _ => true) ?
+        Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
 
 fun use_theories (options, thys) =