--- a/src/Pure/Isar/toplevel.ML Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri May 14 21:32:11 2021 +0200
@@ -79,7 +79,6 @@
val skip_proof_close: transition -> transition
val exec_id: Document_ID.exec -> transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
- val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> state * (exn * string) option
val command_errors: bool -> transition -> state -> Runtime.error list * state option
val command_exception: bool -> transition -> state -> state
@@ -602,19 +601,6 @@
Position.setmp_thread_data pos f x;
-(* post-transition hooks *)
-
-local
- val hooks =
- Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list);
-in
-
-fun add_hook hook = Synchronized.change hooks (cons hook);
-fun get_hooks () = Synchronized.value hooks;
-
-end;
-
-
(* apply transitions *)
local
@@ -634,7 +620,6 @@
val opt_err' = opt_err |> Option.map
(fn Runtime.EXCURSION_FAIL exn_info => exn_info
| exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
- val _ = get_hooks () |> List.app (fn f => ignore \<^try>\<open>f tr st st'\<close>);
in (st', opt_err') end;
end;