# HG changeset patch
# User wenzelm
# Date 1257687516 -3600
# Node ID d066e8369a33cfe74288300163e7e375cafa442b
# Parent  d4d0bee8c36e8b033025bcfd0a5fcb12d212dbf3
print_theorems: suppress concealed (global) facts, unless "!" option is given;

diff -r d4d0bee8c36e -r d066e8369a33 doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Sun Nov 08 13:57:07 2009 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy	Sun Nov 08 14:38:36 2009 +0100
@@ -21,7 +21,7 @@
   \end{matharray}
 
   \begin{rail}
-    'print\_theory' ( '!'?)
+    ('print\_theory' | 'print\_theorems') ('!'?)
     ;
 
     'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
@@ -56,8 +56,8 @@
   \item @{command "print_attributes"} prints all attributes
   available in the current theory context.
   
-  \item @{command "print_theorems"} prints theorems resulting from
-  the last command.
+  \item @{command "print_theorems"} prints theorems resulting from the
+  last command; the ``@{text "!"}'' option indicates extra verbosity.
   
   \item @{command "find_theorems"}~@{text criteria} retrieves facts
   from the theory or proof context matching all of given search
diff -r d4d0bee8c36e -r d066e8369a33 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Sun Nov 08 13:57:07 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Sun Nov 08 14:38:36 2009 +0100
@@ -41,7 +41,7 @@
   \end{matharray}
 
   \begin{rail}
-    'print\_theory' ( '!'?)
+    ('print\_theory' | 'print\_theorems') ('!'?)
     ;
 
     'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
@@ -76,8 +76,8 @@
   \item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}} prints all attributes
   available in the current theory context.
   
-  \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}} prints theorems resulting from
-  the last command.
+  \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}} prints theorems resulting from the
+  last command; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra verbosity.
   
   \item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria} retrieves facts
   from the theory or proof context matching all of given search
diff -r d4d0bee8c36e -r d066e8369a33 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 08 13:57:07 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 08 14:38:36 2009 +0100
@@ -50,7 +50,7 @@
   val print_abbrevs: Toplevel.transition -> Toplevel.transition
   val print_facts: Toplevel.transition -> Toplevel.transition
   val print_configs: Toplevel.transition -> Toplevel.transition
-  val print_theorems: Toplevel.transition -> Toplevel.transition
+  val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
   val print_registrations: string -> Toplevel.transition -> Toplevel.transition
@@ -343,20 +343,20 @@
   ProofContext.setmp_verbose_CRITICAL
     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
 
-val print_theorems_theory = Toplevel.keep (fn state =>
+fun print_theorems_theory verbose = Toplevel.keep (fn state =>
   Toplevel.theory_of state |>
   (case Toplevel.previous_context_of state of
-    SOME prev => Proof_Display.print_theorems_diff (ProofContext.theory_of prev)
-  | NONE => Proof_Display.print_theorems));
+    SOME prev => Proof_Display.print_theorems_diff verbose (ProofContext.theory_of prev)
+  | NONE => Proof_Display.print_theorems verbose));
 
-val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
+fun print_theorems verbose =
+  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
 
 val print_locales = Toplevel.unknown_theory o
   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
 
-fun print_locale (show_facts, name) = Toplevel.unknown_theory o
-  Toplevel.keep (fn state =>
-    Locale.print_locale (Toplevel.theory_of state) show_facts name);
+fun print_locale (verbose, name) = Toplevel.unknown_theory o
+  Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name);
 
 fun print_registrations name = Toplevel.unknown_context o
   Toplevel.keep (fn state =>
diff -r d4d0bee8c36e -r d066e8369a33 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 08 13:57:07 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 08 14:38:36 2009 +0100
@@ -780,7 +780,7 @@
 val _ =
   OuterSyntax.improper_command "print_theorems"
       "print theorems of local theory or proof context" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
+    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
 
 val _ =
   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
diff -r d4d0bee8c36e -r d066e8369a33 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sun Nov 08 13:57:07 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sun Nov 08 14:38:36 2009 +0100
@@ -12,8 +12,8 @@
   val pp_term: theory -> term -> Pretty.T
   val pp_ctyp: ctyp -> Pretty.T
   val pp_cterm: cterm -> Pretty.T
-  val print_theorems_diff: theory -> theory -> unit
-  val print_theorems: theory -> unit
+  val print_theorems_diff: bool -> theory -> theory -> unit
+  val print_theorems: bool -> theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
@@ -46,20 +46,23 @@
 
 (* theorems and theory *)
 
-fun pretty_theorems_diff prev_thys thy =
+fun pretty_theorems_diff verbose prev_thys thy =
   let
     val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
-    val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
+    val facts = PureThy.facts_of thy;
+    val thmss =
+      Facts.dest_static (map PureThy.facts_of prev_thys) facts
+      |> not verbose ? filter_out (Facts.is_concealed facts o #1);
   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
 
-fun print_theorems_diff prev_thy thy =
-  Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
+fun print_theorems_diff verbose prev_thy thy =
+  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
 
-fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
-val print_theorems = Pretty.writeln o pretty_theorems;
+fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
+val print_theorems = Pretty.writeln oo pretty_theorems;
 
 fun pretty_full_theory verbose thy =
-  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
+  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
 
 val print_theory = Pretty.writeln o pretty_full_theory false;