From c112a607a0366d35682e2bb01b4f87053ebb1be3 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 9 Apr 2024 16:13:42 +0200 Subject: [PATCH] fix symbol location within tactic : move the location printing in the Lsp server side --- src/parsing/scope.ml | 11 ++--------- src/pure/pure.ml | 4 +++- 2 files changed, 5 insertions(+), 10 deletions(-) diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 279b68f17..e15f69a97 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -508,15 +508,8 @@ let scope_term : ?find_sym:find_sym -> ?typ:bool -> ?mok:(int -> meta option) -> bool -> sig_state -> env -> p_term -> term = fun ?find_sym ?(typ=false) ?(mok=fun _ -> None) m_term_prv ss env t -> - try - let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in - Bindlib.unbox (scope ?find_sym ~typ 0 md ss env t) - with Fatal(Some p, msg) -> - Console.out 3 (Color.red "[%a]") Pos.pp p; - (** Get ride of the position because the error message is displayed here - There is no more need of the position and this avoids the message - to be displayed twice in [Error.handle_exceptions] *) - raise(Fatal(None, msg)) + let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in + Bindlib.unbox (scope ?find_sym ~typ 0 md ss env t) (** [scope_search_pattern ~find_sym ~typ prv ss env t] turns a pterm [t] meant to be a search patter into a term in the signature state [ss] diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 3cab7c8ce..49ba8098d 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -171,7 +171,9 @@ let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result = let ps, qres = Handle.Tactic.handle ss sym_pos prv (ps, None) tac n in let qres = Option.map (fun f -> f ()) qres in Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres) - with Fatal(p,m) -> Tac_Error(p,m) + with Fatal(Some p,m) -> + Console.out 3 (Color.red "%a") Pos.pp p; + Tac_Error(Some p,m) let end_proof : proof_state -> command_result = fun (_, ss, ps, finalize, _, _) ->