# HG changeset patch
# User wenzelm
# Date 1218653851 -7200
# Node ID fdf43ffceae0f4c1fa8237e156169df50ce5a58f
# Parent  b28b2baada0651f78fde175ad023c6e772f63bc2
removed obsolete present_results;
added theory_results, which is subject to hooks (formerly in present.ML);

diff -r b28b2baada06 -r fdf43ffceae0 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Aug 13 20:57:30 2008 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Aug 13 20:57:31 2008 +0200
@@ -23,12 +23,10 @@
   val print_theorems_diff: theory -> theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T
   val string_of_rule: Proof.context -> string -> thm -> string
-  val print_results: bool -> Proof.context ->
-    ((string * string) * (string * thm list) list) -> unit
-  val present_results: Proof.context ->
-    ((string * string) * (string * thm list) list) -> unit
-  val pretty_consts: Proof.context ->
-    (string * typ -> bool) -> (string * typ) list -> Pretty.T
+  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
+  val add_hook: ((string * thm list) list -> unit) -> unit
+  val theory_results: Proof.context -> ((string * string) * (string * thm list) list) -> unit
+  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
 end
 
 structure ProofDisplay: PROOF_DISPLAY =
@@ -95,6 +93,25 @@
       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
 
+in
+
+fun print_results true = Pretty.writeln oo pretty_results
+  | print_results false = K (K ());
+
+end;
+
+
+(* theory results -- subject to hook *)
+
+local val hooks = ref ([]: ((string * thm list) list -> unit) list) in
+
+fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+fun get_hooks () = CRITICAL (fn () => ! hooks);
+
+end;
+
+local
+
 fun name_results "" res = res
   | name_results name res =
       let
@@ -113,14 +130,14 @@
 
 in
 
-fun print_results true = Pretty.writeln oo pretty_results
-  | print_results false = K (K ());
-
-fun present_results ctxt ((kind, name), res) =
+fun theory_results ctxt ((kind, name), res) =
   if kind = "" orelse kind = Thm.internalK then ()
-  else (print_results true ctxt ((kind, name), res);
-    Context.setmp_thread_data (SOME (Context.Proof ctxt))
-      (Present.results kind) (name_results name res));
+  else
+    let
+      val _ = print_results true ctxt ((kind, name), res);
+      val res' = name_results name res;
+      val _ = List.app (fn f => f res') (get_hooks ());
+    in () end;
 
 end;