# HG changeset patch
# User wenzelm
# Date 1530031491 -7200
# Node ID c6626358bf21ecdc19353a59bd74d7b480deae42
# Parent  795f39bfe4e15029eca0810da434917a7399e53b
tuned signature;

diff -r 795f39bfe4e1 -r c6626358bf21 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Jun 26 17:42:49 2018 +0200
+++ b/src/Pure/Thy/present.ML	Tue Jun 26 18:44:51 2018 +0200
@@ -9,7 +9,7 @@
   val get_bibtex_entries: theory -> string list
   val theory_qualifier: theory -> string
   val document_option: Options.T -> {enabled: bool, disabled: bool}
-  val document_variants: string -> (string * string) list
+  val document_variants: Options.T -> (string * string) list
   val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
   val finish: unit -> unit
@@ -148,14 +148,14 @@
   | "false" => {enabled = false, disabled = true}
   | _ => {enabled = true, disabled = false});
 
-fun document_variants str =
+fun document_variants options =
   let
-    fun read_variant s =
-      (case space_explode "=" s of
-        [name] => (name, "")
-      | [name, tags] => (name, tags)
-      | _ => error ("Malformed document variant specification: " ^ quote s));
-    val variants = map read_variant (space_explode ":" str);
+    val variants =
+      space_explode ":" (Options.string options "document_variants") |> map (fn s =>
+        (case space_explode "=" s of
+          [name] => (name, "")
+        | [name, tags] => (name, tags)
+        | _ => error ("Malformed document variant specification: " ^ quote s)));
     val _ =
       (case duplicates (op =) (map #1 variants) of
         [] => ()
diff -r 795f39bfe4e1 -r c6626358bf21 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Jun 26 17:42:49 2018 +0200
+++ b/src/Pure/Tools/build.ML	Tue Jun 26 18:44:51 2018 +0200
@@ -208,7 +208,7 @@
         browser_info
         (Options.default_string "document")
         (Options.default_string "document_output")
-        (Present.document_variants (Options.default_string "document_variants"))
+        (Present.document_variants (Options.default ()))
         document_files
         graph_file
         parent_name