src/Pure/System/session.ML
changeset 48805 c3ea910b3581
parent 48804 6348e5fca42e
child 48990 12814717c95c
     1.1 --- a/src/Pure/System/session.ML	Tue Aug 14 13:40:49 2012 +0200
     1.2 +++ b/src/Pure/System/session.ML	Tue Aug 14 15:42:58 2012 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    val name: unit -> string
     1.5    val welcome: unit -> string
     1.6    val finish: unit -> unit
     1.7 -  val init: bool -> bool -> bool -> string -> string -> bool -> (string * string) list ->
     1.8 +  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     1.9      string -> string -> string * Present.dump_mode -> string -> bool -> unit
    1.10    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    1.11    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    1.12 @@ -102,10 +102,11 @@
    1.13         remote_path := SOME (Url.explode rpath);
    1.14     (! remote_path, rpath <> ""));
    1.15  
    1.16 -fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
    1.17 +fun init build reset info info_path doc doc_graph doc_output doc_variants
    1.18 +    parent name doc_dump rpath verbose =
    1.19   (init_name reset parent name;
    1.20 -  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
    1.21 -    (path ()) name doc_dump (get_rpath rpath) verbose
    1.22 +  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
    1.23 +    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
    1.24      (map Thy_Info.get_theory (Thy_Info.get_names ())));
    1.25  
    1.26  local
    1.27 @@ -122,7 +123,7 @@
    1.28      name dump rpath level timing verbose max_threads trace_threads
    1.29      parallel_proofs parallel_proofs_threshold =
    1.30    ((fn () =>
    1.31 -     (init build reset info info_path doc doc_graph (read_variants doc_variants) parent name
    1.32 +     (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
    1.33          (doc_dump dump) rpath verbose;
    1.34        with_timing item timing use root;
    1.35        finish ()))