--- a/src/Pure/Isar/session.ML Thu Oct 28 17:11:51 2004 +0200
+++ b/src/Pure/Isar/session.ML Thu Oct 28 19:40:22 2004 +0200
@@ -9,7 +9,7 @@
sig
val name: unit -> string
val welcome: unit -> string
- val use_dir: bool -> string list -> bool -> bool -> string -> bool -> string
+ val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string
-> string -> string -> string -> int -> bool -> unit
val finish: unit -> unit
end;
@@ -67,7 +67,9 @@
(* use_dir *)
+(*
val root_file = ThyLoad.ml_path "ROOT";
+*)
fun get_rpath rpath_str =
(if rpath_str = "" then () else
@@ -77,13 +79,13 @@
rpath := Some (Url.unpack rpath_str);
(!rpath, rpath_str <> ""));
-fun use_dir build modes reset info doc doc_graph parent name dump rpath_str level verbose =
+fun use_dir root_file 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 build info doc doc_graph (path ()) name
(if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
- File.use root_file;
+ File.use (Path.basic root_file);
finish ()))) ()
handle exn => (writeln (Toplevel.exn_message exn); exit 1);