'print_theory': bang option for full verbosity;
authorwenzelm
Tue Sep 19 23:15:26 2006 +0200 (2006-09-19)
changeset 2062129d57880ba00
parent 20620 8b26f58c5646
child 20622 e1a573146be5
'print_theory': bang option for full verbosity;
doc-src/IsarRef/pure.tex
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_display.ML
     1.1 --- a/doc-src/IsarRef/pure.tex	Tue Sep 19 23:15:24 2006 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Tue Sep 19 23:15:26 2006 +0200
     1.3 @@ -1519,9 +1519,10 @@
     1.4  \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
     1.5  \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
     1.6  \indexisarcmd{find-theorems}\indexisarcmd{thm-deps}
     1.7 -\indexisarcmd{print-theorems}
     1.8 +\indexisarcmd{print-theorems}\indexisarcmd{print-theory}
     1.9  \begin{matharray}{rcl}
    1.10    \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
    1.11 +  \isarcmd{print_theory}^* & : & \isarkeep{theory~|~proof} \\
    1.12    \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
    1.13    \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
    1.14    \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
    1.15 @@ -1533,6 +1534,9 @@
    1.16  \end{matharray}
    1.17  
    1.18  \begin{rail}
    1.19 +  'print\_theory' ( '!'?)
    1.20 +  ;
    1.21 +
    1.22    'find\_theorems' (('(' nat ')')?) (criterion *)
    1.23    ;
    1.24    criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
    1.25 @@ -1551,6 +1555,9 @@
    1.26  \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
    1.27    including keywords and command.
    1.28    
    1.29 +\item [$\isarkeyword{print_theory}$] prints the main logical content
    1.30 +  of the theory context; the ``$!$'' option indicates extra verbosity.
    1.31 +
    1.32  \item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and
    1.33    terms, depending on the current context.  The output can be very verbose,
    1.34    including grammar tables and syntax translation rules.  See \cite[\S7,
    1.35 @@ -1568,7 +1575,7 @@
    1.36    In interactive mode this actually refers to the theorems left by the last
    1.37    transaction; this allows to inspect the result of advanced definitional
    1.38    packages, such as $\isarkeyword{datatype}$.
    1.39 -  
    1.40 +
    1.41  \item [$\isarkeyword{find_theorems}~\vec c$] retrieves facts from the theory
    1.42    or proof context matching all of the search criteria $\vec c$.  The
    1.43    criterion $name: p$ selects all theorems whose fully qualified name matches
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 19 23:15:24 2006 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 19 23:15:26 2006 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4    val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
     2.5    val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
     2.6    val print_context: Toplevel.transition -> Toplevel.transition
     2.7 -  val print_theory: Toplevel.transition -> Toplevel.transition
     2.8 +  val print_theory: bool -> Toplevel.transition -> Toplevel.transition
     2.9    val print_syntax: Toplevel.transition -> Toplevel.transition
    2.10    val print_theorems: Toplevel.transition -> Toplevel.transition
    2.11    val print_locales: Toplevel.transition -> Toplevel.transition
    2.12 @@ -218,8 +218,8 @@
    2.13  
    2.14  val print_context = Toplevel.keep Toplevel.print_state_context;
    2.15  
    2.16 -val print_theory = Toplevel.unknown_theory o
    2.17 -  Toplevel.keep (ProofDisplay.print_theory o Toplevel.theory_of);
    2.18 +fun print_theory verbose = Toplevel.unknown_theory o
    2.19 +  Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
    2.20  
    2.21  val print_syntax = Toplevel.unknown_theory o
    2.22    Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 19 23:15:24 2006 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 19 23:15:26 2006 +0200
     3.3 @@ -647,7 +647,7 @@
     3.4  (** diagnostic commands (for interactive mode only) **)
     3.5  
     3.6  val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
     3.7 -
     3.8 +val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
     3.9  
    3.10  val pretty_setmarginP =
    3.11    OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
    3.12 @@ -663,7 +663,7 @@
    3.13  
    3.14  val print_theoryP =
    3.15    OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
    3.16 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory));
    3.17 +    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
    3.18  
    3.19  val print_syntaxP =
    3.20    OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
    3.21 @@ -680,8 +680,7 @@
    3.22  
    3.23  val print_localeP =
    3.24    OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
    3.25 -    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val
    3.26 -      >> (Toplevel.no_timing oo IsarCmd.print_locale));
    3.27 +    (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
    3.28  
    3.29  val print_registrationsP =
    3.30    OuterSyntax.improper_command "print_interps"
     4.1 --- a/src/Pure/Isar/proof_display.ML	Tue Sep 19 23:15:24 2006 +0200
     4.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Sep 19 23:15:26 2006 +0200
     4.3 @@ -21,6 +21,7 @@
     4.4    val pprint_cterm: cterm -> pprint_args -> unit
     4.5    val pprint_thm: thm -> pprint_args -> unit
     4.6    val print_theorems_diff: theory -> theory -> unit
     4.7 +  val print_full_theory: bool -> theory -> unit
     4.8    val string_of_rule: Proof.context -> string -> thm -> string
     4.9    val print_results: bool -> Proof.context ->
    4.10      ((string * string) * (string * thm list) list) -> unit
    4.11 @@ -65,8 +66,10 @@
    4.12  
    4.13  val print_theorems = Pretty.writeln o pretty_theorems;
    4.14  
    4.15 -fun print_theory thy =
    4.16 -  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy]));
    4.17 +fun print_full_theory verbose thy =
    4.18 +  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
    4.19 +
    4.20 +val print_theory = print_full_theory false;
    4.21  
    4.22  
    4.23  (* refinement rule *)