# HG changeset patch
# User wenzelm
# Date 1397727756 -7200
# Node ID d80f43dab30e7f3c5b69c8b7689a6fed1a4ce953
# Parent  3518ea9f5200d58fc30dfe460e5cd87fe6e18939
tuned;

diff -r 3518ea9f5200 -r d80f43dab30e src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Apr 17 11:31:46 2014 +0200
+++ b/src/Pure/Thy/present.ML	Thu Apr 17 11:42:36 2014 +0200
@@ -7,6 +7,7 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
+  val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
@@ -192,7 +193,9 @@
 
 (** document preparation **)
 
-(* document variants *)
+(* options *)
+
+fun document_enabled s = s <> "" andalso s <> "false";
 
 fun document_variants str =
   let
diff -r 3518ea9f5200 -r d80f43dab30e src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Apr 17 11:31:46 2014 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 17 11:42:36 2014 +0200
@@ -99,8 +99,7 @@
 
 fun use_theories last_timing options =
   Thy_Info.use_theories {
-      document =
-        (case Options.string options "document" of "" => false | "false" => false | _ => true),
+      document = Present.document_enabled (Options.string options "document"),
       last_timing = last_timing,
       master_dir = Path.current}
     |> Unsynchronized.setmp print_mode