moved pprint functions to Isar/proof_display.ML;

--- a/src/Pure/Isar/proof_display.ML	Wed Jul 26 00:44:48 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Jul 26 00:44:49 2006 +0200
@@ -14,6 +14,13 @@
 signature PROOF_DISPLAY =
 sig
   include BASIC_PROOF_DISPLAY
+  val debug: bool ref
+  val pprint_context: ProofContext.context -> pprint_args -> unit
+  val pprint_typ: theory -> typ -> pprint_args -> unit
+  val pprint_term: theory -> term -> pprint_args -> unit
+  val pprint_ctyp: ctyp -> pprint_args -> unit
+  val pprint_cterm: cterm -> pprint_args -> unit
+  val pprint_thm: thm -> pprint_args -> unit
   val print_theorems_diff: theory -> theory -> unit
   val string_of_rule: ProofContext.context -> string -> thm -> string
   val print_results: bool -> ProofContext.context ->
@@ -25,6 +32,23 @@
 structure ProofDisplay: PROOF_DISPLAY =
 struct
 
+(* ML toplevel pretty printing *)
+
+val debug = ref false;
+
+fun pprint_context ctxt = Pretty.pprint
+ (if ! debug then
+    Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
+  else Pretty.str "<context>");
+
+fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
+
+val pprint_typ = pprint ProofContext.pretty_typ;
+val pprint_term = pprint ProofContext.pretty_term;
+fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
+fun pprint_thm th = pprint ProofContext.pretty_thm (Thm.theory_of_thm th) th;
+
 
 (* theorems and theory *)
 
@@ -107,4 +131,3 @@
 
 structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
 open BasicProofDisplay;
-

--- a/src/Pure/display.ML	Wed Jul 26 00:44:48 2006 +0200
+++ b/src/Pure/display.ML	Wed Jul 26 00:44:49 2006 +0200
@@ -38,11 +38,8 @@
   val pretty_thms: thm list -> Pretty.T
   val pretty_thm_sg: theory -> thm -> Pretty.T
   val pretty_thms_sg: theory -> thm list -> Pretty.T
-  val pprint_thm: thm -> pprint_args -> unit
   val pretty_ctyp: ctyp -> Pretty.T
-  val pprint_ctyp: ctyp -> pprint_args -> unit
   val pretty_cterm: cterm -> Pretty.T
-  val pprint_cterm: cterm -> pprint_args -> unit
   val pretty_full_theory: theory -> Pretty.T list
   val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
   val pretty_goals: int -> thm -> Pretty.T list
@@ -111,7 +108,6 @@
 
 
 val string_of_thm = Pretty.string_of o pretty_thm;
-val pprint_thm = Pretty.pprint o pretty_thm;
 
 fun pretty_thms [th] = pretty_thm th
   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
@@ -135,9 +131,6 @@
 fun pretty_ctyp cT =
   let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
 
-fun pprint_ctyp cT =
-  let val {thy, T, ...} = rep_ctyp cT in Sign.pprint_typ thy T end;
-
 fun string_of_ctyp cT =
   let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
 
@@ -146,9 +139,6 @@
 fun pretty_cterm ct =
   let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
 
-fun pprint_cterm ct =
-  let val {thy, t, ...} = rep_cterm ct in Sign.pprint_term thy t end;
-
 fun string_of_cterm ct =
   let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
 

--- a/src/Pure/install_pp.ML	Wed Jul 26 00:44:48 2006 +0200
+++ b/src/Pure/install_pp.ML	Wed Jul 26 00:44:49 2006 +0200
@@ -4,10 +4,10 @@
 ML toplevel pretty printing.
 *)
 
-install_pp (make_pp ["Thm", "thm"] Display.pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm);
-install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp);
+install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
+install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
+install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
-install_pp (make_pp ["Context", "proof"] ProofContext.pprint_context);
+install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] (Sign.pprint_typ ProtoPure.thy));
+install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));

--- a/src/Pure/sign.ML	Wed Jul 26 00:44:48 2006 +0200
+++ b/src/Pure/sign.ML	Wed Jul 26 00:44:49 2006 +0200
@@ -143,8 +143,6 @@
   val string_of_sort: theory -> sort -> string
   val string_of_classrel: theory -> class list -> string
   val string_of_arity: theory -> arity -> string
-  val pprint_term: theory -> term -> pprint_args -> unit
-  val pprint_typ: theory -> typ -> pprint_args -> unit
   val pp: theory -> Pretty.pp
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
@@ -398,9 +396,6 @@
 val string_of_classrel = Pretty.string_of oo pretty_classrel;
 val string_of_arity = Pretty.string_of oo pretty_arity;
 
-val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
-val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
-
 fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
   pretty_classrel thy, pretty_arity thy);