# HG changeset patch
# User wenzelm
# Date 975696237 -3600
# Node ID fdde440a90331e4c77331e1a4a282a94b92dae73
# Parent  fc7afc98a329a52cef6cf3daca0702561fe92a36
use_dir: modes;

diff -r fc7afc98a329 -r fdde440a9033 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Fri Dec 01 19:43:40 2000 +0100
+++ b/src/Pure/Isar/session.ML	Fri Dec 01 19:43:57 2000 +0100
@@ -9,7 +9,8 @@
 signature SESSION =
 sig
   val welcome: unit -> string
-  val use_dir: bool -> bool -> string -> string -> string -> string -> string -> unit
+  val use_dir:
+    string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
   val finish: unit -> unit
 end;
 
@@ -75,12 +76,14 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, rpath_str <> ""));
 
-fun use_dir reset info doc parent name dump rpath_str =
-  (init reset parent name;
-   Present.init info doc (path ()) name
-     (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
-   File.symbol_use root_file;
-   finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
+fun use_dir modes reset info doc parent name dump rpath_str =
+  Library.setmp print_mode (modes @ ! print_mode) (fn () =>
+    (init reset parent name;
+     Present.init info doc (path ()) name
+       (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
+     File.symbol_use root_file;
+     finish ())) ()
+  handle exn => (writeln (Toplevel.exn_message exn); exit 1);
 
 
 end;