--- a/src/Pure/Isar/session.ML Tue Oct 23 22:52:45 2001 +0200
+++ b/src/Pure/Isar/session.ML Tue Oct 23 22:53:08 2001 +0200
@@ -10,7 +10,7 @@
sig
val name: unit -> string
val welcome: unit -> string
- val use_dir: string list -> bool -> bool -> string -> bool -> string
+ val use_dir: bool -> string list -> bool -> bool -> string -> bool -> string
-> string -> string -> string -> int -> bool -> unit
val finish: unit -> unit
end;
@@ -78,11 +78,11 @@
rpath := Some (Url.unpack rpath_str);
(!rpath, rpath_str <> ""));
-fun use_dir modes reset info doc doc_graph parent name dump rpath_str level verbose =
+fun use_dir build modes reset info doc doc_graph parent name dump rpath_str level verbose =
Library.setmp print_mode (modes @ ! print_mode)
(Library.setmp Proofterm.proofs level (fn () =>
(init reset parent name;
- Present.init info doc doc_graph (path ()) name
+ Present.init build info doc doc_graph (path ()) name
(if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
File.symbol_use root_file;
finish ()))) ()