# HG changeset patch
# User berghofe
# Date 926953189 -7200
# Node ID 7aa5cc0ae0447f925cf9d9cf21d11abac7823323
# Parent  808a3d9e2404c8b4f9caf060c895fd8cb3f1a287
Changed interface of function use_dir.

diff -r 808a3d9e2404 -r 7aa5cc0ae044 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Mon May 17 16:58:34 1999 +0200
+++ b/src/Pure/Isar/session.ML	Mon May 17 16:59:49 1999 +0200
@@ -8,7 +8,7 @@
 signature SESSION =
 sig
   val welcome: unit -> string
-  val use_dir: bool -> bool -> string -> string -> unit
+  val use_dir: bool -> bool -> string -> string -> string -> unit
   val finish: unit -> unit
 end;
 
@@ -58,9 +58,9 @@
 
 val root_file = ThyLoad.ml_path "ROOT";
 
-fun use_dir reset info parent name =
+fun use_dir reset info parent name rpath =
   (init reset parent name;
-    Present.init info (path ()) name;
+    Present.init info (path ()) name (if rpath = "" then None else Some (Url.unpack rpath));
     File.symbol_use root_file;
     finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);