more direct interpretation of document_variants for build (unchanged for usedir);
authorwenzelm
Tue Aug 14 13:40:49 2012 +0200 (2012-08-14)
changeset 488046348e5fca42e
parent 48795 bece259ee055
child 48805 c3ea910b3581
more direct interpretation of document_variants for build (unchanged for usedir);
src/Pure/System/build.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/System/build.ML	Tue Aug 14 13:01:09 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Aug 14 13:40:49 2012 +0200
     1.3 @@ -65,12 +65,14 @@
     1.4                (pair string ((list (pair Options.decode (list string)))))))))
     1.5            end;
     1.6  
     1.7 +      val document_variants =
     1.8 +        map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
     1.9        val _ =
    1.10          Session.init do_output false
    1.11            (Options.bool options "browser_info") browser_info
    1.12            (Options.string options "document")
    1.13            (Options.bool options "document_graph")
    1.14 -          (space_explode ":" (Options.string options "document_variants"))
    1.15 +          document_variants
    1.16            parent_name name
    1.17            (Options.string options "document_dump",
    1.18              Present.dump_mode (Options.string options "document_dump_mode"))
     2.1 --- a/src/Pure/System/session.ML	Tue Aug 14 13:01:09 2012 +0200
     2.2 +++ b/src/Pure/System/session.ML	Tue Aug 14 13:40:49 2012 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    val name: unit -> string
     2.5    val welcome: unit -> string
     2.6    val finish: unit -> unit
     2.7 -  val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
     2.8 +  val init: bool -> bool -> bool -> string -> string -> bool -> (string * string) list ->
     2.9      string -> string -> string * Present.dump_mode -> string -> bool -> unit
    2.10    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    2.11    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    2.12 @@ -112,13 +112,17 @@
    2.13  
    2.14  fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
    2.15  
    2.16 +fun read_variants strs =
    2.17 +  rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
    2.18 +  |> filter_out (fn (_, s) => s = "-");
    2.19 +
    2.20  in
    2.21  
    2.22  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    2.23      name dump rpath level timing verbose max_threads trace_threads
    2.24      parallel_proofs parallel_proofs_threshold =
    2.25    ((fn () =>
    2.26 -     (init build reset info info_path doc doc_graph doc_variants parent name
    2.27 +     (init build reset info info_path doc doc_graph (read_variants doc_variants) parent name
    2.28          (doc_dump dump) rpath verbose;
    2.29        with_timing item timing use root;
    2.30        finish ()))
     3.1 --- a/src/Pure/Thy/present.ML	Tue Aug 14 13:01:09 2012 +0200
     3.2 +++ b/src/Pure/Thy/present.ML	Tue Aug 14 13:40:49 2012 +0200
     3.3 @@ -19,7 +19,8 @@
     3.4     path: string, parents: string list} list -> unit
     3.5    datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
     3.6    val dump_mode: string -> dump_mode
     3.7 -  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     3.8 +  val read_variant: string -> string * string
     3.9 +  val init: bool -> bool -> string -> string -> bool -> (string * string) list -> string list ->
    3.10      string -> string * dump_mode -> Url.T option * bool -> bool ->
    3.11      theory list -> unit  (*not thread-safe!*)
    3.12    val finish: unit -> unit  (*not thread-safe!*)
    3.13 @@ -274,10 +275,6 @@
    3.14    | [name, tags] => (name, tags)
    3.15    | _ => error ("Malformed document variant specification: " ^ quote str));
    3.16  
    3.17 -fun read_variants strs =
    3.18 -  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
    3.19 -  |> filter_out (fn (_, s) => s = "-");
    3.20 -
    3.21  
    3.22  (* init session *)
    3.23  
    3.24 @@ -299,7 +296,7 @@
    3.25          else if not (can File.check_dir document_path) then
    3.26            (if verbose then Output.physical_stderr "Warning: missing document directory\n"
    3.27             else (); [])
    3.28 -        else read_variants doc_variants;
    3.29 +        else doc_variants;
    3.30  
    3.31        val parent_index_path = Path.append Path.parent index_path;
    3.32        val index_up_lnk =