# HG changeset patch
# User wenzelm
# Date 1397726955 -7200
# Node ID 74851ff8618092a9e55d77857c55663ee9fccb3e
# Parent  eb088da48f868927bb0067ed0f8432f15a6f95a7
tuned;

diff -r eb088da48f86 -r 74851ff86180 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Apr 17 11:13:30 2014 +0200
+++ b/src/Pure/Thy/present.ML	Thu Apr 17 11:29:15 2014 +0200
@@ -7,7 +7,7 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
-  val read_variant: string -> string * string
+  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!*)
   val finish: unit -> unit  (*not thread-safe!*)
@@ -194,11 +194,19 @@
 
 (* document variants *)
 
-fun read_variant str =
-  (case space_explode "=" str of
-    [name] => (name, "")
-  | [name, tags] => (name, tags)
-  | _ => error ("Malformed document variant specification: " ^ quote str));
+fun document_variants str =
+  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 _ =
+      (case duplicates (op =) (map #1 variants) of
+        [] => ()
+      | dups => error ("Duplicate document variants: " ^ commas_quote dups));
+  in variants end;
 
 
 (* init session *)
diff -r eb088da48f86 -r 74851ff86180 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Apr 17 11:13:30 2014 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 17 11:29:15 2014 +0200
@@ -140,13 +140,6 @@
 
       val _ = Options.set_default options;
 
-      val document_variants =
-        map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
-      val _ =
-        (case duplicates (op =) (map fst document_variants) of
-          [] => ()
-        | dups => error ("Duplicate document variants: " ^ commas_quote dups));
-
       val _ = writeln ("\fSession.name = " ^ name);
       val _ =
         Session.init do_output
@@ -155,7 +148,7 @@
           (Options.string options "document")
           (Options.bool options "document_graph")
           (Options.string options "document_output")
-          document_variants
+          (Present.document_variants (Options.string options "document_variants"))
           (map (pairself Path.explode) document_files)
           parent_name (chapter, name)
           verbose;