Skip to content

Commit

Permalink
fix symbol location within tactic : move the location printing in the…
Browse files Browse the repository at this point in the history
… Lsp server side
  • Loading branch information
Alidra committed Apr 9, 2024
1 parent 86f1241 commit c112a60
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 10 deletions.
11 changes: 2 additions & 9 deletions src/parsing/scope.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
4 changes: 3 additions & 1 deletion src/pure/pure.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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, _, _) ->
Expand Down

0 comments on commit c112a60

Please sign in to comment.