# HG changeset patch
# User wenzelm
# Date 1030439221 -7200
# Node ID 131bb248504dc1e6676028e1a6ad4bcf8dd956ed
# Parent  5825aef91ac569e7e3ef3052a9688fc56580d94b
simplified results;
added hook;

diff -r 5825aef91ac5 -r 131bb248504d src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Aug 27 11:06:45 2002 +0200
+++ b/src/Pure/Thy/present.ML	Tue Aug 27 11:07:01 2002 +0200
@@ -25,8 +25,8 @@
   val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
   val theory_output: string -> string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
-  val multi_result: string * (string * thm list) list -> unit
-  val results: string -> string -> thm list -> unit
+  val add_hook: (string -> (string * thm list) list -> unit) -> unit
+  val results: string -> (string * thm list) list -> unit
   val theorem: string -> thm -> unit
   val theorems: string -> thm list -> unit
   val chapter: string -> unit
@@ -469,10 +469,15 @@
   end);
 
 
-fun multi_result res = with_session () (fn _ => with_context add_html (HTML.multi_result res));
-fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
-fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
-fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));
+val hooks = ref ([]: (string -> (string * thm list) list -> unit) list);
+fun add_hook f = hooks := (f :: ! hooks);
+
+fun results k xs =
+ (seq (fn f => (try (fn () => f k xs) (); ())) (! hooks);
+  with_session () (fn _ => with_context add_html (HTML.results k xs)));
+
+fun theorem a th = results "theorem" [(a, [th])];
+fun theorems a ths = results "theorems" [(a, ths)];
 fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
 fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));