# HG changeset patch # User wenzelm # Date 1344944449 -7200 # Node ID 6348e5fca42e89d3a8dc7454472303a16c0a5378 # Parent bece259ee05506e2cfd8482aef5c4beaaf4cb453 more direct interpretation of document_variants for build (unchanged for usedir); diff -r bece259ee055 -r 6348e5fca42e src/Pure/System/build.ML --- 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")) diff -r bece259ee055 -r 6348e5fca42e src/Pure/System/session.ML --- 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 ())) diff -r bece259ee055 -r 6348e5fca42e src/Pure/Thy/present.ML --- 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 =