Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_cmd.ML
changeset 33515 d066e8369a33
parent 33456 fbd47f9b9b12
child 33671 4b0f2599ed48 
--- 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 =>
isabelle