# HG changeset patch
# User wenzelm
# Date 1001586242 -7200
# Node ID 0a2617b311cc7f538f6f2c725569d42bbf72234e
# Parent  43c6735080b806514077f99d416d704850bb6e31
use_dir: verbose option;

diff -r 43c6735080b8 -r 0a2617b311cc src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Thu Sep 27 12:23:23 2001 +0200
+++ b/src/Pure/Isar/session.ML	Thu Sep 27 12:24:02 2001 +0200
@@ -10,8 +10,8 @@
 sig
   val name: unit -> string
   val welcome: unit -> string
-  val use_dir:
-    string list -> bool -> bool -> string -> string -> string -> string -> string -> int -> unit
+  val use_dir: string list -> bool -> bool -> string -> string
+    -> string -> string -> string -> int -> bool -> unit
   val finish: unit -> unit
 end;
 
@@ -78,12 +78,12 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, rpath_str <> ""));
 
-fun use_dir modes reset info doc parent name dump rpath_str level =
+fun use_dir modes reset info doc 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 (path ()) name
-         (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
+         (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
        File.symbol_use root_file;
        finish ()))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);