more direct interpretation of document_variants for build (unchanged for usedir);

--- a/src/Pure/System/build.ML	Tue Aug 14 13:01:09 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Aug 14 13:40:49 2012 +0200
@@ -65,12 +65,14 @@
               (pair string ((list (pair Options.decode (list string)))))))))
           end;
 
+      val document_variants =
+        map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
       val _ =
         Session.init do_output false
           (Options.bool options "browser_info") browser_info
           (Options.string options "document")
           (Options.bool options "document_graph")
-          (space_explode ":" (Options.string options "document_variants"))
+          document_variants
           parent_name name
           (Options.string options "document_dump",
             Present.dump_mode (Options.string options "document_dump_mode"))

--- a/src/Pure/System/session.ML	Tue Aug 14 13:01:09 2012 +0200
+++ b/src/Pure/System/session.ML	Tue Aug 14 13:40:49 2012 +0200
@@ -10,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val finish: unit -> unit
-  val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
+  val init: bool -> bool -> bool -> string -> string -> bool -> (string * string) list ->
     string -> string -> string * Present.dump_mode -> string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
@@ -112,13 +112,17 @@
 
 fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
 
+fun read_variants strs =
+  rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
+  |> filter_out (fn (_, s) => s = "-");
+
 in
 
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
-     (init build reset info info_path doc doc_graph doc_variants parent name
+     (init build reset info info_path doc doc_graph (read_variants doc_variants) parent name
         (doc_dump dump) rpath verbose;
       with_timing item timing use root;
       finish ()))

--- a/src/Pure/Thy/present.ML	Tue Aug 14 13:01:09 2012 +0200
+++ b/src/Pure/Thy/present.ML	Tue Aug 14 13:40:49 2012 +0200
@@ -19,7 +19,8 @@
    path: string, parents: string list} list -> unit
   datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
   val dump_mode: string -> dump_mode
-  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
+  val read_variant: string -> string * string
+  val init: bool -> bool -> string -> string -> bool -> (string * string) list -> string list ->
     string -> string * dump_mode -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
@@ -274,10 +275,6 @@
   | [name, tags] => (name, tags)
   | _ => error ("Malformed document variant specification: " ^ quote str));
 
-fun read_variants strs =
-  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
-  |> filter_out (fn (_, s) => s = "-");
-
 
 (* init session *)
 
@@ -299,7 +296,7 @@
         else if not (can File.check_dir document_path) then
           (if verbose then Output.physical_stderr "Warning: missing document directory\n"
            else (); [])
-        else read_variants doc_variants;
+        else doc_variants;
 
       val parent_index_path = Path.append Path.parent index_path;
       val index_up_lnk =