# HG changeset patch
# User wenzelm
# Date 1313265847 -7200
# Node ID a32ca91659281777e3e427c66f9c1cb9e4a3ae35
# Parent  be78e13a80d6182822e96dd8ab14634a9263db26
less verbosity in batch mode -- spam reduction and notable performance improvement;
clarified Proof_Display.print_consts;

diff -r be78e13a80d6 -r a32ca9165928 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Aug 13 21:28:01 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sat Aug 13 22:04:07 2011 +0200
@@ -125,9 +125,7 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true }
 
-        val _ =
-          if not is_external then ()
-          else Specification.print_consts lthy (K false) (map fst fixes)
+        val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
       in
         (info, 
          lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
diff -r be78e13a80d6 -r a32ca9165928 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 21:28:01 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 22:04:07 2011 +0200
@@ -218,11 +218,11 @@
 (* constant definitions and abbreviations *)
 
 val _ =
-  Outer_Syntax.local_theory "definition" "constant definition" Keyword.thy_decl
-    (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args));
+  Outer_Syntax.local_theory' "definition" "constant definition" Keyword.thy_decl
+    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
 
 val _ =
-  Outer_Syntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
+  Outer_Syntax.local_theory' "abbreviation" "constant abbreviation" Keyword.thy_decl
     (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
       >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
@@ -263,18 +263,18 @@
 (* theorems *)
 
 fun theorems kind =
-  Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
+  Parse_Spec.name_facts >> (fn args => #2 oo Specification.theorems_cmd kind args);
 
 val _ =
-  Outer_Syntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
+  Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
 
 val _ =
-  Outer_Syntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
+  Outer_Syntax.local_theory' "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
 
 val _ =
-  Outer_Syntax.local_theory "declare" "declare theorems" Keyword.thy_decl
+  Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl
     (Parse.and_list1 Parse_Spec.xthms1
-      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
+      >> (fn args => #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
 
 
 (* name space entry path *)
diff -r be78e13a80d6 -r a32ca9165928 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Aug 13 21:28:01 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sat Aug 13 22:04:07 2011 +0200
@@ -18,7 +18,7 @@
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
   val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
-  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
+  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
 end
 
 structure Proof_Display: PROOF_DISPLAY =
@@ -115,13 +115,17 @@
 
 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
 
-in
-
 fun pretty_consts ctxt pred cs =
   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
     [] => pretty_vars ctxt "constants" cs
   | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
 
+in
+
+fun print_consts do_print ctxt pred cs =
+  if not do_print orelse null cs then ()
+  else Pretty.writeln (pretty_consts ctxt pred cs);
+
 end;
 
 end;
diff -r be78e13a80d6 -r a32ca9165928 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Aug 13 21:28:01 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Aug 13 22:04:07 2011 +0200
@@ -7,7 +7,6 @@
 
 signature SPECIFICATION =
 sig
-  val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
   val check_spec:
     (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
@@ -37,23 +36,26 @@
   val definition:
     (binding * typ option * mixfix) option * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory
+  val definition':
+    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
+    bool -> local_theory -> (term * (string * thm)) * local_theory
   val definition_cmd:
     (binding * string option * mixfix) option * (Attrib.binding * string) ->
-    local_theory -> (term * (string * thm)) * local_theory
+    bool -> local_theory -> (term * (string * thm)) * local_theory
   val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
-    local_theory -> local_theory
+    bool -> local_theory -> local_theory
   val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
-    local_theory -> local_theory
+    bool -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory
+    bool -> local_theory -> (string * thm list) list * local_theory
   val theorems_cmd: string ->
     (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory
+    bool -> local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     Element.context_i list -> Element.statement_i ->
@@ -76,12 +78,6 @@
 structure Specification: SPECIFICATION =
 struct
 
-(* diagnostics *)
-
-fun print_consts _ _ [] = ()
-  | print_consts ctxt pred cs = Pretty.writeln (Proof_Display.pretty_consts ctxt pred cs);
-
-
 (* prepare specification *)
 
 local
@@ -166,7 +162,7 @@
 
 (* axiomatization -- within global theory *)
 
-fun gen_axioms do_print prep raw_vars raw_specs thy =
+fun gen_axioms prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
     val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
@@ -188,13 +184,10 @@
       |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
       |> Local_Theory.notes axioms;
 
-    val _ =
-      if not do_print then ()
-      else print_consts facts_lthy (K false) xs;
   in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
 
-val axiomatization = gen_axioms false check_specification;
-val axiomatization_cmd = gen_axioms true read_specification;
+val axiomatization = gen_axioms check_specification;
+val axiomatization_cmd = gen_axioms read_specification;
 
 fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd);
 fun axiom_cmd (b, ax) = axiomatization_cmd [] [(b, [ax])] #>> (hd o hd o snd);
@@ -202,7 +195,7 @@
 
 (* definition *)
 
-fun gen_def do_print prep (raw_var, raw_spec) lthy =
+fun gen_def prep (raw_var, raw_spec) int lthy =
   let
     val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
     val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
@@ -228,18 +221,18 @@
         [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
-    val _ =
-      if not do_print then ()
-      else print_consts lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+
+    val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy4) end;
 
-val definition = gen_def false check_free_spec;
-val definition_cmd = gen_def true read_free_spec;
+val definition' = gen_def check_free_spec;
+fun definition spec = definition' spec false;
+val definition_cmd = gen_def read_free_spec;
 
 
 (* abbreviation *)
 
-fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
+fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
   let
     val ((vars, [(_, prop)]), _) =
       prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
@@ -260,11 +253,11 @@
       |> Local_Theory.abbrev mode (var, rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
 
-    val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
+    val _ = Proof_Display.print_consts int lthy' (K false) [(x, T)];
   in lthy' end;
 
-val abbreviation = gen_abbrev false check_free_spec;
-val abbreviation_cmd = gen_abbrev true read_free_spec;
+val abbreviation = gen_abbrev check_free_spec;
+val abbreviation_cmd = gen_abbrev read_free_spec;
 
 
 (* notation *)
@@ -290,14 +283,14 @@
 
 (* fact statements *)
 
-fun gen_theorems prep_fact prep_att kind raw_facts lthy =
+fun gen_theorems prep_fact prep_att kind raw_facts int lthy =
   let
     val attrib = prep_att (Proof_Context.theory_of lthy);
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts;
-    val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 val theorems = gen_theorems (K I) (K I);
@@ -389,12 +382,12 @@
           (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
           if Binding.is_empty name andalso null atts then
-            (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') = lthy'
                 |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
-              val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
             in lthy'' end)
         |> after_qed results'
       end;
@@ -411,7 +404,8 @@
 
 in
 
-val theorem = gen_theorem false (K I) Expression.cert_statement;
+val theorem' = gen_theorem false (K I) Expression.cert_statement;
+fun theorem a b c d e f = theorem' a b c d e f;
 val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
 
 val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;