added option show_modes to predicate compiler

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Oct 27 09:02:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -114,6 +114,7 @@
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
+      show_modes = chk "show_modes",
       show_mode_inference = chk "show_mode_inference",
       show_compilation = chk "show_compilation",
       skip_proof = chk "skip_proof",
@@ -146,7 +147,7 @@
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
-val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
+val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"]
 
 local structure P = OuterParse

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 27 09:02:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -135,9 +135,10 @@
 datatype options = Options of {  
   expected_modes : (string * int list list) option,
   show_steps : bool,
-  show_mode_inference : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
+  show_mode_inference : bool,
+  show_modes : bool,
   show_compilation : bool,
   skip_proof : bool,
 
@@ -148,9 +149,10 @@
 
 fun expected_modes (Options opt) = #expected_modes opt
 fun show_steps (Options opt) = #show_steps opt
-fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
 fun show_proof_trace (Options opt) = #show_proof_trace opt
+fun show_modes (Options opt) = #show_modes opt
+fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_compilation (Options opt) = #show_compilation opt
 fun skip_proof (Options opt) = #skip_proof opt
 
@@ -163,6 +165,7 @@
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
+  show_modes = false,
   show_mode_inference = false,
   show_compilation = false,
   skip_proof = false,

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:02:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -332,10 +332,12 @@
 
 (* diagnostic display functions *)
 
-fun print_modes modes =
-  Output.tracing ("Inferred modes:\n" ^
-    cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
-      string_of_mode ms)) modes));
+fun print_modes options modes =
+  if show_modes options then
+    Output.tracing ("Inferred modes:\n" ^
+      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+        string_of_mode ms)) modes))
+  else ()
 
 fun print_pred_mode_table string_of_entry thy pred_mode_table =
   let
@@ -2150,7 +2152,7 @@
     val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses 
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes options modes
-    val _ = print_modes modes
+    val _ = print_modes options modes
       (*val _ = print_moded_clauses thy moded_clauses*)
     val _ = print_step options "Defining executable functions..."
     val thy' = fold (#create_definitions steps preds) modes thy