renamed `keep_derivs' to `proofs', and made an integer;

--- a/lib/Tools/usedir	Fri Aug 31 22:46:23 2001 +0200
+++ b/lib/Tools/usedir	Sat Sep 01 00:14:16 2001 +0200
@@ -50,7 +50,7 @@
 MODES=""
 RESET=false
 SESSION=""
-PROOF=MinDeriv
+PROOFS=0
 
 function getoptions()
 {
@@ -84,7 +84,7 @@
         fi
         ;;
       p)
-        PROOF="$OPTARG"
+        PROOFS="$OPTARG"
         ;;
       r)
         RESET=true
@@ -158,7 +158,7 @@
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
-    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOF;" \
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
   RC="$?"
 else
@@ -167,7 +167,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
-    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOF; quit();" \
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS; quit();" \
     -r -q "$LOGIC" > "$LOG" 2>&1
   RC="$?"
   cd ..

--- a/src/HOL/ex/mesontest.ML	Fri Aug 31 22:46:23 2001 +0200
+++ b/src/HOL/ex/mesontest.ML	Sat Sep 01 00:14:16 2001 +0200
@@ -10,7 +10,7 @@
 
 show_hyps := false;
 
-keep_derivs := MinDeriv;
+proofs := 0;
 by (rtac ccontr 1);
 val [prem] = gethyps 1;
 val nnf = make_nnf prem;
@@ -23,7 +23,7 @@
 
 Goal "False";
 by (resolve_tac goes 1);
-keep_derivs := FullDeriv;
+proofs := 2;
 
 by (prolog_step_tac horns 1);
 by (iter_deepen_prolog_tac horns);

--- a/src/Pure/Isar/session.ML	Fri Aug 31 22:46:23 2001 +0200
+++ b/src/Pure/Isar/session.ML	Sat Sep 01 00:14:16 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 -> deriv_kind -> unit
+    string list -> bool -> bool -> string -> string -> string -> string -> string -> int -> unit
   val finish: unit -> unit
 end;
 
@@ -78,14 +78,14 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, 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 ())) ()
+fun use_dir modes reset info doc parent name dump rpath_str level =
+  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);
+       File.symbol_use root_file;
+       finish ()))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);
 
 

--- a/src/Pure/Thy/thm_deps.ML	Fri Aug 31 22:46:23 2001 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Sep 01 00:14:16 2001 +0200
@@ -22,8 +22,8 @@
 
 open Proofterm;
 
-fun enable () = keep_derivs := ThmDeriv;
-fun disable () = keep_derivs := MinDeriv;
+fun enable () = if ! proofs = 0 then proofs := 1 else ();
+fun disable () = proofs := 0;
 
 fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
   | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])

--- a/src/Pure/proofterm.ML	Fri Aug 31 22:46:23 2001 +0200
+++ b/src/Pure/proofterm.ML	Sat Sep 01 00:14:16 2001 +0200
@@ -10,8 +10,7 @@
 
 signature BASIC_PROOFTERM =
 sig
-  datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
-  val keep_derivs : deriv_kind ref
+  val proofs: int ref
 
   datatype proof =
      PBound of int
@@ -171,25 +170,28 @@
 
 (** proof objects with different levels of detail **)
 
-datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
+val proofs = ref 2;
 
-val keep_derivs = ref FullDeriv;
+fun err_illegal_level i =
+  error ("Illegal level of detail for proof objects: " ^ string_of_int i);
 
 fun if_ora b = if b then oracles_of_proof else K;
 
 fun infer_derivs f (ora1, prf1) (ora2, prf2) =
   (ora1 orelse ora2, 
-   case !keep_derivs of
-     FullDeriv => f prf1 prf2
-   | ThmDeriv => MinProof (mk_min_proof (mk_min_proof ([], prf1), prf2))
-   | MinDeriv => MinProof (if_ora ora2 (if_ora ora1 [] prf1) prf2));
+   case !proofs of
+     2 => f prf1 prf2
+   | 1 => MinProof (mk_min_proof (mk_min_proof ([], prf1), prf2))
+   | 0 => MinProof (if_ora ora2 (if_ora ora1 [] prf1) prf2)
+   | i => err_illegal_level i);
 
 fun infer_derivs' f (ora, prf) =
   (ora,
-   case !keep_derivs of
-     FullDeriv => f prf
-   | ThmDeriv => MinProof (mk_min_proof ([], prf))
-   | MinDeriv => MinProof (if_ora ora [] prf));
+   case !proofs of
+     2 => f prf
+   | 1 => MinProof (mk_min_proof ([], prf))
+   | 0 => MinProof (if_ora ora [] prf)
+   | i => err_illegal_level i);
 
 fun (prf %%% t) = prf %% Some t;
 
@@ -978,7 +980,7 @@
     val args = map (fn (v as Var (ixn, _)) =>
         if ixn mem nvs then Some v else None) (vars_of prop) @
       map Some (sort (make_ord atless) (term_frees prop));
-    val opt_prf = if !keep_derivs=FullDeriv then
+    val opt_prf = if ! proofs = 2 then
         #4 (shrink [] 0 (rewrite_prf fst (!(ProofData.get_sg sign))
           (foldr (uncurry implies_intr_proof) (hyps', prf))))
       else MinProof (mk_min_proof ([], prf));