# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID 2fef4f9429f79947870bd0f2c468d8050281e7f4
# Parent  5378e61add1a1fd4d0ebe4699c8bb1abdd47bbeb
added option show_intermediate_results

diff -r 5378e61add1a -r 2fef4f9429f7 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,7 +112,7 @@
   (*check_modes : (string * int list list) list,*)
   show_steps : bool,
   show_mode_inference : bool,
-  
+  show_intermediate_results : bool,
   (*
   inductify_functions : bool,
   *)
@@ -120,13 +120,16 @@
   rpred : bool
 };
 
-fun is_show_steps (Options opt) = #show_steps opt
+fun show_steps (Options opt) = #show_steps opt
+fun show_intermediate_results (Options opt) = #show_intermediate_results opt
+
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt
 
 
 val default_options = Options {
   show_steps = false,
+  show_intermediate_results = false,
   show_mode_inference = false,
   inductify = false,
   rpred = false
@@ -134,7 +137,7 @@
 
 
 fun print_step options s =
-  if is_show_steps options then tracing s else ()
+  if show_steps options then tracing s else ()
   
 
 (* tuple processing *)
diff -r 5378e61add1a -r 2fef4f9429f7 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
@@ -26,11 +26,13 @@
 
 fun tracing s = ()
 
-fun print_intross thy msg intross =
-  tracing (msg ^ 
+fun print_intross options thy msg intross =
+  if show_intermediate_results options then
+   Output.tracing (msg ^ 
     (space_implode "; " (map 
       (fn intros => commas (map (Display.string_of_thm_global thy) intros)) intross)))
-
+  else ()
+      
 fun print_specs thy specs =
   map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
     ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
@@ -41,7 +43,7 @@
     val specs = map (apsnd (map
       (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs
     val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy')
-    val _ = print_intross thy'' "Flattened introduction rules: " intross1
+    val _ = print_intross options thy'' "Flattened introduction rules: " intross1
     val _ =  "Replacing functions in introrules..."
     val intross2 =
       if fail_safe_mode then
@@ -49,7 +51,7 @@
           SOME intross => intross
         | NONE => let val _ = warning "Function replacement failed!" in intross1 end
       else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
-    val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2
+    val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2
     val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..."
     val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
     val (new_intross, thy'''')  =
@@ -77,12 +79,12 @@
     val _ = print_specs thy' fun_pred_specs
     val specs = (get_specs prednames) @ fun_pred_specs
     val (intross3, thy''') = process_specification options specs thy'
-    val _ = print_intross thy''' "Introduction rules with new constants: " intross3
+    val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
     val intross4 = map (maps remove_pointless_clauses) intross3
-    val _ = print_intross thy''' "After removing pointless clauses: " intross4
+    val _ = print_intross options thy''' "After removing pointless clauses: " intross4
     val intross5 = map (map (AxClass.overload thy''')) intross4
     val intross6 = burrow (map (expand_tuples thy''')) intross5
-    val _ = print_intross thy''' "introduction rules before registering: " intross6
+    val _ = print_intross options thy''' "introduction rules before registering: " intross6
     val _ = print_step options "Registering introduction rules..."
     val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
   in
@@ -105,6 +107,7 @@
   in
     Options {
       show_steps = chk "show_steps",
+      show_intermediate_results = chk "show_intermediate_results",
       show_mode_inference = chk "show_mode_inference",
       inductify = chk "inductify",
       rpred = chk "rpred"
@@ -135,7 +138,7 @@
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
-val bool_options = ["show_steps", "show_mode_inference", "inductify", "rpred"]
+val bool_options = ["show_steps", "show_intermediate_results", "show_mode_inference", "inductify", "rpred"]
 
 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)