# HG changeset patch
# User wenzelm
# Date 1248130579 -7200
# Node ID 39acf19e9f3a36425c732f537362f33efed06d28
# Parent  568a23753e3a8fe150c1c10fd19655282142b0f5
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
removed some very old thm print operations;

diff -r 568a23753e3a -r 39acf19e9f3a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 20 21:20:09 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 21 00:56:19 2009 +0200
@@ -36,13 +36,8 @@
   val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
-  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
-  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
   val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
-  val pretty_thm: Proof.context -> thm -> Pretty.T
-  val pretty_thms: Proof.context -> thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
-  val string_of_thm: Proof.context -> thm -> string
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
@@ -293,31 +288,18 @@
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
-fun pretty_thm_aux ctxt show_status th =
-  let
-    val flags = {quote = false, show_hyps = true, show_status = show_status};
-    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
-  in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
-
-fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
-  | pretty_thms_aux ctxt flag ths =
-      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
-
 fun pretty_fact_name ctxt a = Pretty.block
   [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
 
-fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
+fun pretty_fact_aux ctxt flag ("", ths) =
+      Display.pretty_thms_aux ctxt flag ths
   | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
-      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
+      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
   | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
-      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
+      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
 
-fun pretty_thm ctxt = pretty_thm_aux ctxt true;
-fun pretty_thms ctxt = pretty_thms_aux ctxt true;
 fun pretty_fact ctxt = pretty_fact_aux ctxt true;
 
-val string_of_thm = Pretty.string_of oo pretty_thm;
-
 
 
 (** prepare types **)
@@ -1369,7 +1351,7 @@
       val suppressed = len - ! prems_limit;
       val prt_prems = if null prems then []
         else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
-          map (pretty_thm ctxt) (Library.drop (suppressed, prems)))];
+          map (Display.pretty_thm ctxt) (Library.drop (suppressed, prems)))];
     in prt_structs @ prt_fixes @ prt_prems end;
 
 
diff -r 568a23753e3a -r 39acf19e9f3a src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Jul 20 21:20:09 2009 +0200
+++ b/src/Pure/display.ML	Tue Jul 21 00:56:19 2009 +0200
@@ -16,18 +16,17 @@
 signature DISPLAY =
 sig
   include BASIC_DISPLAY
-  val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
+  val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     term list -> thm -> Pretty.T
-  val pretty_thm: thm -> Pretty.T
-  val string_of_thm: thm -> string
-  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 print_thm: thm -> unit
-  val print_thms: thm list -> unit
-  val prth: thm -> thm
-  val prthq: thm Seq.seq -> thm Seq.seq
-  val prths: thm list -> thm list
+  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
+  val pretty_thm: Proof.context -> thm -> Pretty.T
+  val pretty_thm_global: theory -> thm -> Pretty.T
+  val pretty_thm_without_context: thm -> Pretty.T
+  val string_of_thm: Proof.context -> thm -> string
+  val string_of_thm_global: theory -> thm -> string
+  val string_of_thm_without_context: thm -> string
+  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
+  val pretty_thms: Proof.context -> thm list -> Pretty.T
   val pretty_ctyp: ctyp -> Pretty.T
   val string_of_ctyp: ctyp -> string
   val print_ctyp: ctyp -> unit
@@ -69,7 +68,7 @@
         else ""
       end;
 
-fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
+fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
   let
     val th = Thm.strip_shyps raw_th;
     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
@@ -96,27 +95,33 @@
       else [Pretty.brk 1, pretty_tags tags];
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
-fun pretty_thm th =
-  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
-    {quote = true, show_hyps = false, show_status = true} [] th;
-
-val string_of_thm = Pretty.string_of o pretty_thm;
-
-fun pretty_thms [th] = pretty_thm th
-  | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
-
-val pretty_thm_sg = pretty_thm oo Thm.transfer;
-val pretty_thms_sg = pretty_thms oo (map o Thm.transfer);
+fun pretty_thm_aux ctxt show_status th =
+  let
+    val flags = {quote = false, show_hyps = true, show_status = show_status};
+    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
+  in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
 
 
-(* top-level commands for printing theorems *)
+fun pretty_thm ctxt = pretty_thm_aux ctxt true;
+
+fun pretty_thm_global thy th =
+  pretty_thm_raw (Syntax.pp_global thy)
+    {quote = false, show_hyps = false, show_status = true} [] th;
+
+fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
 
-val print_thm = Pretty.writeln o pretty_thm;
-val print_thms = Pretty.writeln o pretty_thms;
+val string_of_thm = Pretty.string_of oo pretty_thm;
+val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
+val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context;
+
 
-fun prth th = (print_thm th; th);
-fun prthq thq = (Seq.print (K print_thm) 100000 thq; thq);
-fun prths ths = (prthq (Seq.of_list ths); ths);
+(* multiple theorems *)
+
+fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
+  | pretty_thms_aux ctxt flag ths =
+      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
+
+fun pretty_thms ctxt = pretty_thms_aux ctxt true;
 
 
 (* other printing commands *)