--- 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
--- 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
--- 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 =>
--- 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
--- 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;