clarified print operations for "terms" and "theorems";
authorwenzelm
Mon May 05 17:14:46 2014 +0200 (2014-05-05 ago)
changeset 56868b5fb264d53ba
parent 56867 224109105008
child 56869 6e26ae897bad
clarified print operations for "terms" and "theorems";
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	Mon May 05 16:30:19 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 05 17:14:46 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 print_theorems: bool -> Toplevel.transition -> Toplevel.transition
     1.8 +  val pretty_theorems: bool -> Toplevel.state -> Pretty.T
     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 @@ -258,20 +258,19 @@
    1.13      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    1.14  
    1.15  
    1.16 -(* print theorems *)
    1.17 -
    1.18 -fun print_theorems_proof verbose =
    1.19 -  Toplevel.keep (fn st =>
    1.20 -    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
    1.21 +(* theorems of theory or proof context *)
    1.22  
    1.23 -fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    1.24 -  Toplevel.theory_of state |>
    1.25 -  (case Toplevel.previous_context_of state of
    1.26 -    SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
    1.27 -  | NONE => Proof_Display.print_theorems verbose));
    1.28 -
    1.29 -fun print_theorems verbose =
    1.30 -  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
    1.31 +fun pretty_theorems verbose st =
    1.32 +  if Toplevel.is_proof st then
    1.33 +    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
    1.34 +  else
    1.35 +    let
    1.36 +      val thy = Toplevel.theory_of st;
    1.37 +      val prev_thys =
    1.38 +        (case Toplevel.previous_context_of st of
    1.39 +          SOME prev => [Proof_Context.theory_of prev]
    1.40 +        | NONE => Theory.parents_of thy);
    1.41 +    in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
    1.42  
    1.43  
    1.44  (* display dependencies *)
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 05 16:30:19 2014 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 05 17:14:46 2014 +0200
     2.3 @@ -817,7 +817,8 @@
     2.4  val _ =
     2.5    Outer_Syntax.improper_command @{command_spec "print_theorems"}
     2.6      "print theorems of local theory or proof context"
     2.7 -    (opt_bang >> Isar_Cmd.print_theorems);
     2.8 +    (opt_bang >> (fn b =>
     2.9 +      Toplevel.unknown_context o Toplevel.keep (Pretty.writeln 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	Mon May 05 16:30:19 2014 +0200
     3.2 +++ b/src/Pure/Isar/proof_display.ML	Mon May 05 17:14:46 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 print_theorems_diff: bool -> theory -> theory -> unit
     3.8 -  val print_theorems: bool -> theory -> unit
     3.9 +  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
    3.10 +  val pretty_theorems: bool -> theory -> Pretty.T
    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 @@ -66,11 +66,8 @@
    3.15      val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
    3.16    in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    3.17  
    3.18 -fun print_theorems_diff verbose prev_thy thy =
    3.19 -  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
    3.20 -
    3.21 -fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    3.22 -val print_theorems = Pretty.writeln oo pretty_theorems;
    3.23 +fun pretty_theorems verbose thy =
    3.24 +  pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    3.25  
    3.26  fun pretty_full_theory verbose thy =
    3.27    Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
     4.1 --- a/src/Pure/Tools/print_operation.ML	Mon May 05 16:30:19 2014 +0200
     4.2 +++ b/src/Pure/Tools/print_operation.ML	Mon May 05 17:14:46 2014 +0200
     4.3 @@ -69,14 +69,12 @@
     4.4      (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
     4.5  
     4.6  val _ =
     4.7 -  register "binds" "term bindings of proof context"
     4.8 +  register "terms" "term bindings of proof context"
     4.9      (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
    4.10  
    4.11  val _ =
    4.12 -  register "facts" "facts of proof context"
    4.13 -    (fn st =>
    4.14 -      Proof_Context.pretty_local_facts (Toplevel.context_of st) false
    4.15 -      |> Pretty.chunks |> Pretty.string_of);
    4.16 +  register "theorems" "theorems of local theory or proof context"
    4.17 +    (Pretty.string_of o Isar_Cmd.pretty_theorems false);
    4.18  
    4.19  val _ =
    4.20    register "state" "proof state"