--- 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 *)
--- 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;