diff --git a/src/kernel_services/analysis/logic_interp.mli b/src/kernel_services/analysis/logic_interp.mli index 5020269dbe052c9cfb72c94ca36cc2a49dc89e8e..739821d75e5c0bfaaeec7ed8ec41f1f396323ec8 100644 --- a/src/kernel_services/analysis/logic_interp.mli +++ b/src/kernel_services/analysis/logic_interp.mli @@ -28,4 +28,5 @@ module To_zone : sig val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref end -exception Error of location * string +exception [@alert deprecated "Use directly Logic_parse_string.Error istead."] + Error of location * string diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml index 31d005daf3e195dac525dbafe363ac52e7ba978c..bf1e67a56dc187a7b5f551ef625ba0e5d6bc13a5 100644 --- a/src/plugins/eva/gui/register_gui.ml +++ b/src/plugins/eva/gui/register_gui.ml @@ -340,7 +340,7 @@ module Select (Eval: Eval) = struct let pred = !Db.Properties.Interp.predicate ~env kf txt in select_predicate main_ui loc pred with - | Logic_interp.Error (_, mess) -> + | Logic_parse_string.Error (_, mess) -> main_ui#error "Invalid %a: %s" pp_term_or_pred tp mess | Parsing.Parse_error -> main_ui#error "Invalid %a: Parse error" pp_term_or_pred tp diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 1abf9ab1efbf4e4770fe1f41c422085f0397eef8..29dd1f33eaf1e03f480a1ce8d8ddbcd64d3461a2 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -41,8 +41,8 @@ module Cache = Hashtbl.Make(Key) let get_term kf term = let env = logic_environment () in - try Some (!Db.Properties.Interp.term ~env kf term) - with Logic_interp.Error _ | Parsing.Parse_error -> None + try Some (Logic_parse_string.term ~env kf term) + with Logic_parse_string.Error _ | Parsing.Parse_error -> None let key_of_localizable = let open Printer_tag in diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml index 7bdf6c01161551dac897a8076f0e7664630573f4..08ac01fac909ba02cf25ebc3862df4be347eed4c 100644 --- a/src/plugins/slicing/slicingCmds.ml +++ b/src/plugins/slicing/slicingCmds.ml @@ -685,7 +685,7 @@ let add_persistent_cmdline () = SlicingParameters.Select.WrAccess.clear () ; end; add_persistent_selection !selection; - with Logic_interp.Error(_loc,msg) -> + with Logic_parse_string.Error(_loc,msg) -> SlicingParameters.warning ~wkey:SlicingParameters.wkey_cmdline "%s. Slicing requests from the command line are ignored." msg end;