# HG changeset patch
# User wenzelm
# Date 1220386824 -7200
# Node ID 7eaf0813bdc3da8594ea03a60a3593e5b43b226e
# Parent  5f340fb49b9094f0f7444e08ba60bf6519217c76
added add_hook interface for post-transition hooks;

diff -r 5f340fb49b90 -r 7eaf0813bdc3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Sep 02 22:20:21 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Sep 02 22:20:24 2008 +0200
@@ -88,6 +88,7 @@
   val unknown_context: transition -> transition
   val status: transition -> Markup.T -> unit
   val error_msg: transition -> exn * string -> unit
+  val add_hook: (transition -> state -> state * (exn * string) option -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val commit_exit: transition
   val excursion: transition list -> unit
@@ -612,6 +613,16 @@
   setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) ();
 
 
+(* post-transition hooks *)
+
+local val hooks = ref ([]: (transition -> state -> state * (exn * string) option -> unit) list) in
+
+fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+fun get_hooks () = CRITICAL (fn () => ! hooks);
+
+end;
+
+
 (* apply transitions *)
 
 local
@@ -635,13 +646,19 @@
 in
 
 fun transition int tr st =
-  let val ctxt = try context_of st in
-    (case app int tr st of
-      (_, SOME TERMINATE) => NONE
-    | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
-    | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
-    | (state', NONE) => SOME (state', NONE))
-  end;
+  let
+    val hooks = get_hooks ();
+    fun apply_hooks st_err = hooks |> List.app (fn f => (try (fn () => f tr st st_err) (); ()));
+
+    val ctxt = try context_of st;
+    val res =
+      (case app int tr st of
+        (_, SOME TERMINATE) => NONE
+      | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
+      | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
+      | (state', NONE) => SOME (state', NONE));
+    val _ = Option.map apply_hooks res;
+  in res end;
 
 end;