src/Pure/Isar/proof_display.ML
changeset 20211 c7f907f41f7c
parent 19482 9f11af8f7ef9
child 20235 3cbf73ed92f8
     1.1 --- a/src/Pure/Isar/proof_display.ML	Wed Jul 26 00:44:48 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Jul 26 00:44:49 2006 +0200
     1.3 @@ -14,6 +14,13 @@
     1.4  signature PROOF_DISPLAY =
     1.5  sig
     1.6    include BASIC_PROOF_DISPLAY
     1.7 +  val debug: bool ref
     1.8 +  val pprint_context: ProofContext.context -> pprint_args -> unit
     1.9 +  val pprint_typ: theory -> typ -> pprint_args -> unit
    1.10 +  val pprint_term: theory -> term -> pprint_args -> unit
    1.11 +  val pprint_ctyp: ctyp -> pprint_args -> unit
    1.12 +  val pprint_cterm: cterm -> pprint_args -> unit
    1.13 +  val pprint_thm: thm -> pprint_args -> unit
    1.14    val print_theorems_diff: theory -> theory -> unit
    1.15    val string_of_rule: ProofContext.context -> string -> thm -> string
    1.16    val print_results: bool -> ProofContext.context ->
    1.17 @@ -25,6 +32,23 @@
    1.18  structure ProofDisplay: PROOF_DISPLAY =
    1.19  struct
    1.20  
    1.21 +(* ML toplevel pretty printing *)
    1.22 +
    1.23 +val debug = ref false;
    1.24 +
    1.25 +fun pprint_context ctxt = Pretty.pprint
    1.26 + (if ! debug then
    1.27 +    Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    1.28 +  else Pretty.str "<context>");
    1.29 +
    1.30 +fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
    1.31 +
    1.32 +val pprint_typ = pprint ProofContext.pretty_typ;
    1.33 +val pprint_term = pprint ProofContext.pretty_term;
    1.34 +fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.35 +fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.36 +fun pprint_thm th = pprint ProofContext.pretty_thm (Thm.theory_of_thm th) th;
    1.37 +
    1.38  
    1.39  (* theorems and theory *)
    1.40  
    1.41 @@ -107,4 +131,3 @@
    1.42  
    1.43  structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
    1.44  open BasicProofDisplay;
    1.45 -