pretty_thm_aux etc.: explicit show_status flag;

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 26 14:14:02 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 26 15:18:50 2009 +0100
@@ -36,6 +36,9 @@
   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
@@ -295,21 +298,28 @@
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
-fun pretty_thm ctxt th =
-  let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
-  in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
+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 ctxt [th] = pretty_thm ctxt th
-  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
+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 ctxt ("", ths) = pretty_thms ctxt ths
-  | pretty_fact ctxt (a, [th]) = Pretty.block
-      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th]
-  | pretty_fact ctxt (a, ths) = Pretty.block
-      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths));
+fun pretty_fact_aux ctxt flag ("", ths) = 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_aux ctxt flag (a, ths) = Pretty.block
+      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (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;
 

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 26 14:14:02 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 26 15:18:50 2009 +0100
@@ -655,13 +655,9 @@
                                   text=[XML.Elem("pgml",[],
                                                  maps YXML.parse_body strings)] })
 
-        fun string_of_thm th = Pretty.string_of
-                                   (Display.pretty_thm_aux
-                                        (Syntax.pp_global (Thm.theory_of_thm th))
-                                        false (* quote *)
-                                        false (* show hyps *)
-                                        [] (* asms *)
-                                        th)
+        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
+            (Syntax.pp_global (Thm.theory_of_thm th))
+            {quote = false, show_hyps = false, show_status = true} [] th)
 
         fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
 

--- a/src/Pure/display.ML	Thu Mar 26 14:14:02 2009 +0100
+++ b/src/Pure/display.ML	Thu Mar 26 15:18:50 2009 +0100
@@ -17,7 +17,8 @@
 sig
   include BASIC_DISPLAY
   val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
-  val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
+  val pretty_thm_aux: 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
@@ -57,19 +58,20 @@
 fun pretty_flexpair pp (t, u) = Pretty.block
   [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
 
-fun display_status th =
-  let
-    val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
-    val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
-  in
-    if failed then "!!"
-    else if oracle andalso unfinished then "!?"
-    else if oracle then "!"
-    else if unfinished then "?"
-    else ""
-  end;
+fun display_status false _ = ""
+  | display_status true th =
+      let
+        val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
+        val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
+      in
+        if failed then "!!"
+        else if oracle andalso unfinished then "!?"
+        else if oracle then "!"
+        else if unfinished then "?"
+        else ""
+      end;
 
-fun pretty_thm_aux pp quote show_hyps' asms raw_th =
+fun pretty_thm_aux 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;
@@ -80,7 +82,7 @@
     val prt_term = q o Pretty.term pp;
 
     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
-    val status = display_status th;
+    val status = display_status show_status th;
 
     val hlen = length xshyps + length hyps' + length tpairs;
     val hsymbs =
@@ -97,7 +99,8 @@
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
 fun pretty_thm th =
-  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] 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;