# HG changeset patch
# User berghofe
# Date 999267768 -7200
# Node ID 4db3876f1224c4c2b6e8fb01a305bfc0f7fda640
# Parent  b2e4077979b597aff5cc93a558d04e706fb11bcc
Added new argument to use_dir for derivation kind.

diff -r b2e4077979b5 -r 4db3876f1224 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Fri Aug 31 16:22:02 2001 +0200
+++ b/src/Pure/Isar/session.ML	Fri Aug 31 16:22:48 2001 +0200
@@ -11,7 +11,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val use_dir:
-    string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
+    string list -> bool -> bool -> string -> string -> string -> string -> string -> deriv_kind -> unit
   val finish: unit -> unit
 end;
 
@@ -78,11 +78,12 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, rpath_str <> ""));
 
-fun use_dir modes reset info doc parent name dump rpath_str =
+fun use_dir modes reset info doc parent name dump rpath_str der =
   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);
+     Proofterm.keep_derivs := der;
      File.symbol_use root_file;
      finish ())) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);