diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml index 26eba1a5c8a2c268a1dde6583886f0e9582e12e7..44387df98db283851b6dab4b53edc6b0ac31d21c 100644 --- a/src/kernel_services/ast_data/property_status.ml +++ b/src/kernel_services/ast_data/property_status.ml @@ -392,6 +392,13 @@ module Register_hook = Hook.Build (struct type t = Property.t end) let register_property_add_hook = Register_hook.extend +module Status_hook = Hook.Build + (struct type t = emitter_with_properties * Property.t * emitted_status end) + +let register_status_update_hook f = + Status_hook.extend + (fun (emitter, property, status) -> f emitter property status) + let rec register ppt = Kernel.debug ~dkey:Kernel.dkey_prop_status_reg "REGISTERING %a in %a" @@ -486,6 +493,7 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s = add { emitter with properties = [ reach_ppt ] } s | _ :: _ -> Kernel.fatal "Emitter %a proves invalidity of %a under \ hypotheses: unsound!" Emitter.pretty e Property.pretty ppt)); + Status_hook.apply (emitter, ppt, s); s in (try diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli index bbe2f162668e8d475022dc3730dd77d5d541cd79..a16f5bcbfb5263f6405d9486dd8cb415637181c9 100644 --- a/src/kernel_services/ast_data/property_status.mli +++ b/src/kernel_services/ast_data/property_status.mli @@ -138,6 +138,11 @@ val fold_on_statuses: Property.t -> 'a -> 'a +val register_status_update_hook: + (emitter_with_properties -> Property.t -> emitted_status -> unit) -> unit +(** Registers an hook to be called each time a property status is emitted. + @since Frama-C+dev *) + (* ************************************************************************ *) (** {2 Consolidated status} *) (* ************************************************************************ *)