# HG changeset patch
# User wenzelm
# Date 1406030580 -7200
# Node ID 8e0a7eaffe47b2619949e9ab7ad9434b49740da7
# Parent  30885e25c6de101c8499a3bf7a6130a29ce2e70b
tuned messages;

diff -r 30885e25c6de -r 8e0a7eaffe47 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 22 13:36:51 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 22 14:03:00 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 pretty_theorems: bool -> Toplevel.state -> Pretty.T
+  val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
@@ -262,7 +262,7 @@
 
 fun pretty_theorems verbose st =
   if Toplevel.is_proof st then
-    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
+    Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose
   else
     let
       val thy = Toplevel.theory_of st;
diff -r 30885e25c6de -r 8e0a7eaffe47 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 22 13:36:51 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 22 14:03:00 2014 +0200
@@ -811,7 +811,8 @@
   Outer_Syntax.improper_command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
     (opt_bang >> (fn b =>
-      Toplevel.unknown_context o Toplevel.keep (Pretty.writeln o Isar_Cmd.pretty_theorems b)));
+      Toplevel.unknown_context o
+      Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locales"}
diff -r 30885e25c6de -r 8e0a7eaffe47 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Jul 22 13:36:51 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Jul 22 14:03:00 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 pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
-  val pretty_theorems: bool -> theory -> Pretty.T
+  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
+  val pretty_theorems: bool -> theory -> Pretty.T list
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
@@ -65,13 +65,14 @@
     val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
     val facts = Global_Theory.facts_of thy;
     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;
+    val prts = map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss));
+  in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
 
 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]);
+  Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy);
 
 val print_theory = Pretty.writeln o pretty_full_theory false;
 
diff -r 30885e25c6de -r 8e0a7eaffe47 src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Tue Jul 22 13:36:51 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Tue Jul 22 14:03:00 2014 +0200
@@ -64,7 +64,8 @@
   register "context" "context of local theory target" Toplevel.pretty_context;
 
 val _ =
-  register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of);
+  register "cases" "cases of proof context"
+    (Proof_Context.pretty_cases o Toplevel.context_of);
 
 val _ =
   register "terms" "term bindings of proof context"
@@ -72,7 +73,7 @@
 
 val _ =
   register "theorems" "theorems of local theory or proof context"
-    (single o Isar_Cmd.pretty_theorems false);
+    (Isar_Cmd.pretty_theorems false);
 
 val _ =
   register "state" "proof state" Toplevel.pretty_state;