tuned ProofDisplay.pretty_full_theory;
authorwenzelm
Tue May 08 17:40:20 2007 +0200 (2007-05-08)
changeset 22872d7189dc8939c
parent 22871 9ffb43b19ec6
child 22873 decd2ff5f503
tuned ProofDisplay.pretty_full_theory;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue May 08 17:40:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue May 08 17:40:20 2007 +0200
     1.3 @@ -432,7 +432,7 @@
     1.4  val print_context = Toplevel.keep Toplevel.print_state_context;
     1.5  
     1.6  fun print_theory verbose = Toplevel.unknown_theory o
     1.7 -  Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
     1.8 +  Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of);
     1.9  
    1.10  val print_syntax = Toplevel.unknown_context o
    1.11    Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
     2.1 --- a/src/Pure/Isar/proof_display.ML	Tue May 08 17:40:18 2007 +0200
     2.2 +++ b/src/Pure/Isar/proof_display.ML	Tue May 08 17:40:20 2007 +0200
     2.3 @@ -21,14 +21,14 @@
     2.4    val pprint_cterm: cterm -> pprint_args -> unit
     2.5    val pprint_thm: thm -> pprint_args -> unit
     2.6    val print_theorems_diff: theory -> theory -> unit
     2.7 -  val print_full_theory: bool -> theory -> unit
     2.8    val pretty_full_theory: bool -> theory -> Pretty.T
     2.9    val string_of_rule: Proof.context -> string -> thm -> string
    2.10    val print_results: bool -> Proof.context ->
    2.11      ((string * string) * (string * thm list) list) -> unit
    2.12    val present_results: Proof.context ->
    2.13      ((string * string) * (string * thm list) list) -> unit
    2.14 -  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
    2.15 +  val pretty_consts: Proof.context ->
    2.16 +    (string * typ -> bool) -> (string * typ) list -> Pretty.T
    2.17  end
    2.18  
    2.19  structure ProofDisplay: PROOF_DISPLAY =
    2.20 @@ -47,7 +47,7 @@
    2.21  val pprint_term = pprint ProofContext.pretty_term;
    2.22  fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    2.23  fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    2.24 -val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
    2.25 +val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
    2.26  
    2.27  
    2.28  (* theorems and theory *)
    2.29 @@ -68,13 +68,10 @@
    2.30  
    2.31  val print_theorems = Pretty.writeln o pretty_theorems;
    2.32  
    2.33 -fun print_full_theory verbose thy =
    2.34 -  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
    2.35 +fun pretty_full_theory verbose thy =
    2.36 +  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    2.37  
    2.38 -val print_theory = print_full_theory false;
    2.39 -
    2.40 -fun pretty_full_theory verbose thy =
    2.41 -    Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    2.42 +val print_theory = Pretty.writeln o pretty_full_theory false;
    2.43  
    2.44  
    2.45  (* refinement rule *)