# HG changeset patch
# User wenzelm
# Date 1158700526 -7200
# Node ID 29d57880ba00595bb4caceac88921981c8ef8d86
# Parent  8b26f58c5646ee81da4761777342dedb092d1ccf
'print_theory': bang option for full verbosity;

diff -r 8b26f58c5646 -r 29d57880ba00 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Sep 19 23:15:24 2006 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Sep 19 23:15:26 2006 +0200
@@ -1519,9 +1519,10 @@
 \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
 \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
 \indexisarcmd{find-theorems}\indexisarcmd{thm-deps}
-\indexisarcmd{print-theorems}
+\indexisarcmd{print-theorems}\indexisarcmd{print-theory}
 \begin{matharray}{rcl}
   \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
+  \isarcmd{print_theory}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
@@ -1533,6 +1534,9 @@
 \end{matharray}
 
 \begin{rail}
+  'print\_theory' ( '!'?)
+  ;
+
   'find\_theorems' (('(' nat ')')?) (criterion *)
   ;
   criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
@@ -1551,6 +1555,9 @@
 \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
   including keywords and command.
   
+\item [$\isarkeyword{print_theory}$] prints the main logical content
+  of the theory context; the ``$!$'' option indicates extra verbosity.
+
 \item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and
   terms, depending on the current context.  The output can be very verbose,
   including grammar tables and syntax translation rules.  See \cite[\S7,
@@ -1568,7 +1575,7 @@
   In interactive mode this actually refers to the theorems left by the last
   transaction; this allows to inspect the result of advanced definitional
   packages, such as $\isarkeyword{datatype}$.
-  
+
 \item [$\isarkeyword{find_theorems}~\vec c$] retrieves facts from the theory
   or proof context matching all of the search criteria $\vec c$.  The
   criterion $name: p$ selects all theorems whose fully qualified name matches
diff -r 8b26f58c5646 -r 29d57880ba00 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 19 23:15:24 2006 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 19 23:15:26 2006 +0200
@@ -43,7 +43,7 @@
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
-  val print_theory: Toplevel.transition -> Toplevel.transition
+  val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
@@ -218,8 +218,8 @@
 
 val print_context = Toplevel.keep Toplevel.print_state_context;
 
-val print_theory = Toplevel.unknown_theory o
-  Toplevel.keep (ProofDisplay.print_theory o Toplevel.theory_of);
+fun print_theory verbose = Toplevel.unknown_theory o
+  Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
 
 val print_syntax = Toplevel.unknown_theory o
   Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
diff -r 8b26f58c5646 -r 29d57880ba00 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 19 23:15:24 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 19 23:15:26 2006 +0200
@@ -647,7 +647,7 @@
 (** diagnostic commands (for interactive mode only) **)
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
+val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
 
 val pretty_setmarginP =
   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
@@ -663,7 +663,7 @@
 
 val print_theoryP =
   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory));
+    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
 
 val print_syntaxP =
   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
@@ -680,8 +680,7 @@
 
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
-    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val
-      >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val print_registrationsP =
   OuterSyntax.improper_command "print_interps"
diff -r 8b26f58c5646 -r 29d57880ba00 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 19 23:15:24 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 19 23:15:26 2006 +0200
@@ -21,6 +21,7 @@
   val pprint_cterm: cterm -> pprint_args -> unit
   val pprint_thm: thm -> pprint_args -> unit
   val print_theorems_diff: theory -> theory -> unit
+  val print_full_theory: bool -> theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
   val print_results: bool -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
@@ -65,8 +66,10 @@
 
 val print_theorems = Pretty.writeln o pretty_theorems;
 
-fun print_theory thy =
-  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy]));
+fun print_full_theory verbose thy =
+  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
+
+val print_theory = print_full_theory false;
 
 
 (* refinement rule *)