src/Pure/Isar/proof_display.ML
changeset 30628 4078276bcace
parent 30364 577edc39b501
child 30724 2e54e89bcce7
     1.1 --- a/src/Pure/Isar/proof_display.ML	Sat Mar 21 20:00:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Mar 21 20:00:23 2009 +0100
     1.3 @@ -6,12 +6,12 @@
     1.4  
     1.5  signature PROOF_DISPLAY =
     1.6  sig
     1.7 -  val pprint_context: Proof.context -> pprint_args -> unit
     1.8 -  val pprint_typ: theory -> typ -> pprint_args -> unit
     1.9 -  val pprint_term: theory -> term -> pprint_args -> unit
    1.10 -  val pprint_ctyp: ctyp -> pprint_args -> unit
    1.11 -  val pprint_cterm: cterm -> pprint_args -> unit
    1.12 -  val pprint_thm: thm -> pprint_args -> unit
    1.13 +  val pp_context: Proof.context -> Pretty.T
    1.14 +  val pp_thm: thm -> Pretty.T
    1.15 +  val pp_typ: theory -> typ -> Pretty.T
    1.16 +  val pp_term: theory -> term -> Pretty.T
    1.17 +  val pp_ctyp: ctyp -> Pretty.T
    1.18 +  val pp_cterm: cterm -> Pretty.T
    1.19    val print_theorems_diff: theory -> theory -> unit
    1.20    val print_theorems: theory -> unit
    1.21    val pretty_full_theory: bool -> theory -> Pretty.T
    1.22 @@ -26,18 +26,20 @@
    1.23  
    1.24  (* toplevel pretty printing *)
    1.25  
    1.26 -fun pprint_context ctxt = Pretty.pprint
    1.27 +fun pp_context ctxt =
    1.28   (if ! ProofContext.debug then
    1.29      Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    1.30    else Pretty.str "<context>");
    1.31  
    1.32 -fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
    1.33 +fun pp_thm th =
    1.34 +  let val thy = Thm.theory_of_thm th
    1.35 +  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
    1.36  
    1.37 -val pprint_typ = pprint Syntax.pretty_typ;
    1.38 -val pprint_term = pprint Syntax.pretty_term;
    1.39 -fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.40 -fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.41 -val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
    1.42 +val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
    1.43 +val pp_term = Pretty.quote oo Syntax.pretty_term_global;
    1.44 +
    1.45 +fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.46 +fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.47  
    1.48  
    1.49  (* theorems and theory *)