# 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;