# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID eb91ec1ef6f03b87f74b5d91f1488e653ea5fe8f
# Parent  bb8806eb5da7698bb896b7d7f9f5d9e7ec1e68a3
added option show_proof_trace

diff -r bb8806eb5da7 -r eb91ec1ef6f0 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -112,6 +112,7 @@
   (*check_modes : (string * int list list) list,*)
   show_steps : bool,
   show_mode_inference : bool,
+  show_proof_trace : bool,
   show_intermediate_results : bool,
   (*
   inductify_functions : bool,
@@ -122,6 +123,7 @@
 
 fun show_steps (Options opt) = #show_steps opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
+fun show_proof_trace (Options opt) = #show_proof_trace opt
 
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt
@@ -130,6 +132,7 @@
 val default_options = Options {
   show_steps = false,
   show_intermediate_results = false,
+  show_proof_trace = false,
   show_mode_inference = false,
   inductify = false,
   rpred = false
diff -r bb8806eb5da7 -r eb91ec1ef6f0 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -108,6 +108,7 @@
     Options {
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
+      show_proof_trace = chk "show_proof_trace",
       show_mode_inference = chk "show_mode_inference",
       inductify = chk "inductify",
       rpred = chk "rpred"
@@ -138,7 +139,8 @@
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
-val bool_options = ["show_steps", "show_intermediate_results", "show_mode_inference", "inductify", "rpred"]
+val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
+  "show_mode_inference", "inductify", "rpred"]
 
 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)
 
diff -r bb8806eb5da7 -r eb91ec1ef6f0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -122,6 +122,9 @@
 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
 
 fun print_tac s = Seq.single;
+fun print_tac' options s = 
+  if show_proof_trace options then Tactical.print_tac s else Seq.single;
+
 fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
 
 val do_proofs = Unsynchronized.ref true;
@@ -2137,7 +2140,7 @@
 
 (** proof procedure **)
 
-fun prove_pred thy clauses preds modes pred mode (moded_clauses, compiled_term) =
+fun prove_pred options thy clauses preds modes pred mode (moded_clauses, compiled_term) =
   let
     val ctxt = ProofContext.init thy
     val clauses = the (AList.lookup (op =) clauses pred)
@@ -2146,11 +2149,11 @@
       (if !do_proofs then
         (fn _ =>
         rtac @{thm pred_iffI} 1
-				THEN print_tac "after pred_iffI"
+				THEN print_tac' options "after pred_iffI"
         THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
-        THEN print_tac "proved one direction"
+        THEN print_tac' options "proved one direction"
         THEN prove_other_direction thy modes pred mode moded_clauses
-        THEN print_tac "proved other direction")
+        THEN print_tac' options "proved other direction")
       else (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy))
   end;
 
@@ -2174,11 +2177,11 @@
   map_preds_modes (fn pred => compile_pred compfuns mk_fun_of use_size thy all_vs param_vs pred
       (the (AList.lookup (op =) preds pred))) moded_clauses  
   
-fun prove thy clauses preds modes moded_clauses compiled_terms =
-  map_preds_modes (prove_pred thy clauses preds modes)
+fun prove options thy clauses preds modes moded_clauses compiled_terms =
+  map_preds_modes (prove_pred options thy clauses preds modes)
     (join_preds_modes moded_clauses compiled_terms)
 
-fun prove_by_skip thy _ _ _ _ compiled_terms =
+fun prove_by_skip options thy _ _ _ _ compiled_terms =
   map_preds_modes (fn pred => fn mode => fn t => Drule.standard (setmp quick_and_dirty true (SkipProof.make_thm thy) t))
     compiled_terms
 
@@ -2321,7 +2324,7 @@
       (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
     val _ = print_compiled_terms thy' compiled_terms
     val _ = print_step options "Proving equations..."
-    val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
+    val result_thms = #prove steps options thy' clauses preds (extra_modes @ modes)
       moded_clauses compiled_terms
     val qname = #qname steps
     (* val attrib = gn thy => Attrib.attribute_i thy Code.add_eqn_attrib *)