--- 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;
--- 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"}
--- 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;
--- 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;