diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml index 8869fe97088901d6ae11313b3bb9cb474203aec4..56739c79dd7706fde593cbef832fe22275d1d18c 100644 --- a/src/kernel_services/ast_data/annotations.ml +++ b/src/kernel_services/ast_data/annotations.ml @@ -365,14 +365,7 @@ let code_annot_emitter ?filter stmt = try let tbl = Code_annots.find stmt in let filter e l acc = - let e = - try Emitter.Usable_emitter.get e - with Not_found -> - (* in some cases, e.g. when loading a state with a different set - of plugins loaded, the original emitter might not be available, - leading to discarding annotations. Let the kernel adopt them. *) - Emitter.orphan - in + let e = Emitter.Usable_emitter.get e in match filter with | None -> List.map (fun a -> a, e) l @ acc | Some f -> diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml index 7d53caca822ba2d876124301f2334e7f62e1bd98..9f5ada97cc5e2a407f0dd6ea0b06003a43b9a9d9 100644 --- a/src/kernel_services/plugin_entry_points/emitter.ml +++ b/src/kernel_services/plugin_entry_points/emitter.ml @@ -155,7 +155,7 @@ module Usable_emitter = struct let mem_project = Datatype.never_any_project end) - let get e = + let unsafe_get e = let get_params map = Datatype.String.Map.fold (fun s _ acc -> Typed_parameter.get s :: acc) @@ -167,6 +167,13 @@ module Usable_emitter = struct correctness_parameters = get_params e.correctness_values; tuning_parameters = get_params e.tuning_values } + (* In some cases, e.g. when loading a state with a different set + of plugins loaded, the original emitter might not be available, + leading to discarding annotations. Let the kernel adopt them. *) + let get e = + try unsafe_get e + with Not_found -> orphan + let get_name e = e.u_name let get_unique_name e = Format.asprintf "%a" pretty e