moved pprint functions to Isar/proof_display.ML;
authorwenzelm
Wed Jul 26 00:44:49 2006 +0200 (2006-07-26)
changeset 20211c7f907f41f7c
parent 20210 8fe4ae4360eb
child 20212 f4a8b4e2fb29
moved pprint functions to Isar/proof_display.ML;
src/Pure/Isar/proof_display.ML
src/Pure/display.ML
src/Pure/install_pp.ML
src/Pure/sign.ML
     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 -
     2.1 --- a/src/Pure/display.ML	Wed Jul 26 00:44:48 2006 +0200
     2.2 +++ b/src/Pure/display.ML	Wed Jul 26 00:44:49 2006 +0200
     2.3 @@ -38,11 +38,8 @@
     2.4    val pretty_thms: thm list -> Pretty.T
     2.5    val pretty_thm_sg: theory -> thm -> Pretty.T
     2.6    val pretty_thms_sg: theory -> thm list -> Pretty.T
     2.7 -  val pprint_thm: thm -> pprint_args -> unit
     2.8    val pretty_ctyp: ctyp -> Pretty.T
     2.9 -  val pprint_ctyp: ctyp -> pprint_args -> unit
    2.10    val pretty_cterm: cterm -> Pretty.T
    2.11 -  val pprint_cterm: cterm -> pprint_args -> unit
    2.12    val pretty_full_theory: theory -> Pretty.T list
    2.13    val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
    2.14    val pretty_goals: int -> thm -> Pretty.T list
    2.15 @@ -111,7 +108,6 @@
    2.16  
    2.17  
    2.18  val string_of_thm = Pretty.string_of o pretty_thm;
    2.19 -val pprint_thm = Pretty.pprint o pretty_thm;
    2.20  
    2.21  fun pretty_thms [th] = pretty_thm th
    2.22    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    2.23 @@ -135,9 +131,6 @@
    2.24  fun pretty_ctyp cT =
    2.25    let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
    2.26  
    2.27 -fun pprint_ctyp cT =
    2.28 -  let val {thy, T, ...} = rep_ctyp cT in Sign.pprint_typ thy T end;
    2.29 -
    2.30  fun string_of_ctyp cT =
    2.31    let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
    2.32  
    2.33 @@ -146,9 +139,6 @@
    2.34  fun pretty_cterm ct =
    2.35    let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
    2.36  
    2.37 -fun pprint_cterm ct =
    2.38 -  let val {thy, t, ...} = rep_cterm ct in Sign.pprint_term thy t end;
    2.39 -
    2.40  fun string_of_cterm ct =
    2.41    let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
    2.42  
     3.1 --- a/src/Pure/install_pp.ML	Wed Jul 26 00:44:48 2006 +0200
     3.2 +++ b/src/Pure/install_pp.ML	Wed Jul 26 00:44:49 2006 +0200
     3.3 @@ -4,10 +4,10 @@
     3.4  ML toplevel pretty printing.
     3.5  *)
     3.6  
     3.7 -install_pp (make_pp ["Thm", "thm"] Display.pprint_thm);
     3.8 -install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm);
     3.9 -install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp);
    3.10 +install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
    3.11 +install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
    3.12 +install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
    3.13  install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
    3.14 -install_pp (make_pp ["Context", "proof"] ProofContext.pprint_context);
    3.15 +install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
    3.16  install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    3.17 -install_pp (make_pp ["typ"] (Sign.pprint_typ ProtoPure.thy));
    3.18 +install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
     4.1 --- a/src/Pure/sign.ML	Wed Jul 26 00:44:48 2006 +0200
     4.2 +++ b/src/Pure/sign.ML	Wed Jul 26 00:44:49 2006 +0200
     4.3 @@ -143,8 +143,6 @@
     4.4    val string_of_sort: theory -> sort -> string
     4.5    val string_of_classrel: theory -> class list -> string
     4.6    val string_of_arity: theory -> arity -> string
     4.7 -  val pprint_term: theory -> term -> pprint_args -> unit
     4.8 -  val pprint_typ: theory -> typ -> pprint_args -> unit
     4.9    val pp: theory -> Pretty.pp
    4.10    val arity_number: theory -> string -> int
    4.11    val arity_sorts: theory -> string -> sort -> sort list
    4.12 @@ -398,9 +396,6 @@
    4.13  val string_of_classrel = Pretty.string_of oo pretty_classrel;
    4.14  val string_of_arity = Pretty.string_of oo pretty_arity;
    4.15  
    4.16 -val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
    4.17 -val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
    4.18 -
    4.19  fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
    4.20    pretty_classrel thy, pretty_arity thy);
    4.21