# HG changeset patch
# User wenzelm
# Date 1343227262 -7200
# Node ID bf7f434b91d70eb1e4cd6188d1c93316b66c5425
# Parent  d648225071dd32b86c65b939f131bb5435fbe518
clarified no_document situation;

diff -r d648225071dd -r bf7f434b91d7 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Wed Jul 25 12:40:17 2012 +0200
+++ b/src/Pure/System/build.ML	Wed Jul 25 16:41:02 2012 +0200
@@ -14,6 +14,10 @@
 
 local
 
+fun no_document options =
+  (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso
+  (Options.string options "document_dump" = "");
+
 fun use_thys options =
   Thy_Info.use_thys
     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
@@ -24,8 +28,7 @@
         (Options.int options "parallel_proofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
-    |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
-        Present.no_document
+    |> no_document options ? Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     |> Unsynchronized.setmp Printer.show_question_marks_default
         (Options.bool options "show_question_marks")