# HG changeset patch
# User wenzelm
# Date 1399302886 -7200
# Node ID b5fb264d53baf4ee5412bd12794e750073b49475
# Parent  2241091050084596ec4e689c9723e5aa1e0bc9c0
clarified print operations for "terms" and "theorems";

diff -r 224109105008 -r b5fb264d53ba src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon May 05 16:30:19 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon May 05 17:14:46 2014 +0200
@@ -35,7 +35,7 @@
   val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
-  val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
+  val pretty_theorems: bool -> Toplevel.state -> Pretty.T
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
@@ -258,20 +258,19 @@
     (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
 
 
-(* print theorems *)
-
-fun print_theorems_proof verbose =
-  Toplevel.keep (fn st =>
-    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
+(* theorems of theory or proof context *)
 
-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 verbose (Proof_Context.theory_of prev)
-  | NONE => Proof_Display.print_theorems verbose));
-
-fun print_theorems verbose =
-  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
+fun pretty_theorems verbose st =
+  if Toplevel.is_proof st then
+    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
+  else
+    let
+      val thy = Toplevel.theory_of st;
+      val prev_thys =
+        (case Toplevel.previous_context_of st of
+          SOME prev => [Proof_Context.theory_of prev]
+        | NONE => Theory.parents_of thy);
+    in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
 
 
 (* display dependencies *)
diff -r 224109105008 -r b5fb264d53ba src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon May 05 16:30:19 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon May 05 17:14:46 2014 +0200
@@ -817,7 +817,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
-    (opt_bang >> Isar_Cmd.print_theorems);
+    (opt_bang >> (fn b =>
+      Toplevel.unknown_context o Toplevel.keep (Pretty.writeln o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locales"}
diff -r 224109105008 -r b5fb264d53ba src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon May 05 16:30:19 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon May 05 17:14:46 2014 +0200
@@ -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: bool -> theory -> theory -> unit
-  val print_theorems: bool -> theory -> unit
+  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
+  val pretty_theorems: bool -> theory -> Pretty.T
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
@@ -66,11 +66,8 @@
     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
 
-fun print_theorems_diff verbose prev_thy thy =
-  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
-
-fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
-val print_theorems = Pretty.writeln oo pretty_theorems;
+fun pretty_theorems verbose thy =
+  pretty_theorems_diff verbose (Theory.parents_of thy) thy;
 
 fun pretty_full_theory verbose thy =
   Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
diff -r 224109105008 -r b5fb264d53ba src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Mon May 05 16:30:19 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Mon May 05 17:14:46 2014 +0200
@@ -69,14 +69,12 @@
     (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
 
 val _ =
-  register "binds" "term bindings of proof context"
+  register "terms" "term bindings of proof context"
     (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
 
 val _ =
-  register "facts" "facts of proof context"
-    (fn st =>
-      Proof_Context.pretty_local_facts (Toplevel.context_of st) false
-      |> Pretty.chunks |> Pretty.string_of);
+  register "theorems" "theorems of local theory or proof context"
+    (Pretty.string_of o Isar_Cmd.pretty_theorems false);
 
 val _ =
   register "state" "proof state"