tuned messages;
authorwenzelm
Tue Jul 22 14:03:00 2014 +0200 (2014-07-22 ago)
changeset 576058e0a7eaffe47
parent 57604 30885e25c6de
child 57606 6df377afda4a
tuned messages;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_display.ML
src/Pure/Tools/print_operation.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 22 13:36:51 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 22 14:03:00 2014 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     1.5    val diag_state: Proof.context -> Toplevel.state
     1.6    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     1.7 -  val pretty_theorems: bool -> Toplevel.state -> Pretty.T
     1.8 +  val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     1.9    val thy_deps: Toplevel.transition -> Toplevel.transition
    1.10    val locale_deps: Toplevel.transition -> Toplevel.transition
    1.11    val class_deps: Toplevel.transition -> Toplevel.transition
    1.12 @@ -262,7 +262,7 @@
    1.13  
    1.14  fun pretty_theorems verbose st =
    1.15    if Toplevel.is_proof st then
    1.16 -    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
    1.17 +    Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose
    1.18    else
    1.19      let
    1.20        val thy = Toplevel.theory_of st;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 22 13:36:51 2014 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 22 14:03:00 2014 +0200
     2.3 @@ -811,7 +811,8 @@
     2.4    Outer_Syntax.improper_command @{command_spec "print_theorems"}
     2.5      "print theorems of local theory or proof context"
     2.6      (opt_bang >> (fn b =>
     2.7 -      Toplevel.unknown_context o Toplevel.keep (Pretty.writeln o Isar_Cmd.pretty_theorems b)));
     2.8 +      Toplevel.unknown_context o
     2.9 +      Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
    2.10  
    2.11  val _ =
    2.12    Outer_Syntax.improper_command @{command_spec "print_locales"}
     3.1 --- a/src/Pure/Isar/proof_display.ML	Tue Jul 22 13:36:51 2014 +0200
     3.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Jul 22 14:03:00 2014 +0200
     3.3 @@ -12,8 +12,8 @@
     3.4    val pp_term: theory -> term -> Pretty.T
     3.5    val pp_ctyp: ctyp -> Pretty.T
     3.6    val pp_cterm: cterm -> Pretty.T
     3.7 -  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
     3.8 -  val pretty_theorems: bool -> theory -> Pretty.T
     3.9 +  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
    3.10 +  val pretty_theorems: bool -> theory -> Pretty.T list
    3.11    val pretty_full_theory: bool -> theory -> Pretty.T
    3.12    val print_theory: theory -> unit
    3.13    val string_of_rule: Proof.context -> string -> thm -> string
    3.14 @@ -65,13 +65,14 @@
    3.15      val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
    3.16      val facts = Global_Theory.facts_of thy;
    3.17      val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
    3.18 -  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    3.19 +    val prts = map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss));
    3.20 +  in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
    3.21  
    3.22  fun pretty_theorems verbose thy =
    3.23    pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    3.24  
    3.25  fun pretty_full_theory verbose thy =
    3.26 -  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
    3.27 +  Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy);
    3.28  
    3.29  val print_theory = Pretty.writeln o pretty_full_theory false;
    3.30  
     4.1 --- a/src/Pure/Tools/print_operation.ML	Tue Jul 22 13:36:51 2014 +0200
     4.2 +++ b/src/Pure/Tools/print_operation.ML	Tue Jul 22 14:03:00 2014 +0200
     4.3 @@ -64,7 +64,8 @@
     4.4    register "context" "context of local theory target" Toplevel.pretty_context;
     4.5  
     4.6  val _ =
     4.7 -  register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of);
     4.8 +  register "cases" "cases of proof context"
     4.9 +    (Proof_Context.pretty_cases o Toplevel.context_of);
    4.10  
    4.11  val _ =
    4.12    register "terms" "term bindings of proof context"
    4.13 @@ -72,7 +73,7 @@
    4.14  
    4.15  val _ =
    4.16    register "theorems" "theorems of local theory or proof context"
    4.17 -    (single o Isar_Cmd.pretty_theorems false);
    4.18 +    (Isar_Cmd.pretty_theorems false);
    4.19  
    4.20  val _ =
    4.21    register "state" "proof state" Toplevel.pretty_state;