added add_hook interface for post-transition hooks;
authorwenzelm
Tue Sep 02 22:20:24 2008 +0200 (2008-09-02)
changeset 280957eaf0813bdc3
parent 28094 5f340fb49b90
child 28096 046418f64474
added add_hook interface for post-transition hooks;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Sep 02 22:20:21 2008 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Sep 02 22:20:24 2008 +0200
     1.3 @@ -88,6 +88,7 @@
     1.4    val unknown_context: transition -> transition
     1.5    val status: transition -> Markup.T -> unit
     1.6    val error_msg: transition -> exn * string -> unit
     1.7 +  val add_hook: (transition -> state -> state * (exn * string) option -> unit) -> unit
     1.8    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.9    val commit_exit: transition
    1.10    val excursion: transition list -> unit
    1.11 @@ -612,6 +613,16 @@
    1.12    setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) ();
    1.13  
    1.14  
    1.15 +(* post-transition hooks *)
    1.16 +
    1.17 +local val hooks = ref ([]: (transition -> state -> state * (exn * string) option -> unit) list) in
    1.18 +
    1.19 +fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    1.20 +fun get_hooks () = CRITICAL (fn () => ! hooks);
    1.21 +
    1.22 +end;
    1.23 +
    1.24 +
    1.25  (* apply transitions *)
    1.26  
    1.27  local
    1.28 @@ -635,13 +646,19 @@
    1.29  in
    1.30  
    1.31  fun transition int tr st =
    1.32 -  let val ctxt = try context_of st in
    1.33 -    (case app int tr st of
    1.34 -      (_, SOME TERMINATE) => NONE
    1.35 -    | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
    1.36 -    | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
    1.37 -    | (state', NONE) => SOME (state', NONE))
    1.38 -  end;
    1.39 +  let
    1.40 +    val hooks = get_hooks ();
    1.41 +    fun apply_hooks st_err = hooks |> List.app (fn f => (try (fn () => f tr st st_err) (); ()));
    1.42 +
    1.43 +    val ctxt = try context_of st;
    1.44 +    val res =
    1.45 +      (case app int tr st of
    1.46 +        (_, SOME TERMINATE) => NONE
    1.47 +      | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
    1.48 +      | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
    1.49 +      | (state', NONE) => SOME (state', NONE));
    1.50 +    val _ = Option.map apply_hooks res;
    1.51 +  in res end;
    1.52  
    1.53  end;
    1.54