Skip to content

Commit

Permalink
Fix the list of messages to be displayed in terminal due to position …
Browse files Browse the repository at this point in the history
…error (#1150)

When executing get_logs, the use of `<`instead of `<=` prevents the last message to be displayed in the terminal (this is partially described in issue #1144 )

Besides, the calculation of position in `do_goals` is moved to `get_goals` because it is redundant with the ones in `get_logs`.

Note one could as well remove this code from `get_logs` and keep it in `do_goals` for efficiency. However, it is safer and **probably** better to call it in the functions actually using the position (namely `get_logs` and `get_goals`)
  • Loading branch information
Alidra authored Nov 18, 2024
1 parent a67c0be commit d926581
Showing 1 changed file with 20 additions and 19 deletions.
39 changes: 20 additions & 19 deletions src/lsp/lp_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -235,18 +235,6 @@ let get_node_at_pos doc line pos =
res
) doc.Lp_doc.nodes

let rec get_goals ~doc ~line ~pos =
let node = get_node_at_pos doc line pos in
let goals = match node with
| None -> Some([], None)
| Some n ->
closest_before (line+1, pos) n.goals in
match goals with
| None -> begin match node with
| None -> None
| Some _ -> get_goals ~doc ~line:(line-1) ~pos:0 end
| Some (v,_) -> Some v

(** [get_first_error doc] returns the first error inferred from doc.logs *)
let get_first_error doc =
List.fold_left (fun acc b ->
Expand All @@ -262,6 +250,25 @@ let get_first_error doc =
(bpos.start_line, bpos.start_col) <= 0 then
acc else Some b) None doc.Lp_doc.logs

let rec get_goals ~doc ~line ~pos =
let (line,pos) =
match get_first_error doc with
| Some ((_,_), Some errpos) ->
let errpos = (errpos.start_line, errpos.start_col) in
if compare errpos (line, pos) <= 0 then errpos else (line, pos)
| _ -> (line,pos)
in
let node = get_node_at_pos doc line pos in
let goals = match node with
| None -> Some([], None)
| Some n ->
closest_before (line+1, pos) n.goals in
match goals with
| None -> begin match node with
| None -> None
| Some _ -> get_goals ~doc ~line:(line-1) ~pos:0 end
| Some (v,_) -> Some v

let get_logs ~doc ~line ~pos : string =
(* DEBUG LOG START *)
LIO.log_error "get_logs"
Expand Down Expand Up @@ -294,7 +301,7 @@ let get_logs ~doc ~line ~pos : string =
(fun ((_,msg),loc) ->
match loc with
| Some Pos.{start_line; start_col; _}
when compare (start_line,start_col) end_limit < 0 -> Some msg
when compare (start_line,start_col) end_limit <= 0 -> Some msg
| _ -> None)
doc.Lp_doc.logs
in
Expand All @@ -303,12 +310,6 @@ let get_logs ~doc ~line ~pos : string =
let do_goals ofmt ~id params =
let uri, line, pos = get_docTextPosition params in
let doc = Hashtbl.find completed_table uri in
let line, pos = match get_first_error doc with
| Some ((_, _), Some loc) ->
let eline, epos = loc.start_line, loc.start_col in
if compare (eline, epos) (line, pos) <= 0 then
eline, epos else line, pos
| _ -> line, pos in
let goals = get_goals ~doc ~line ~pos in
let logs = get_logs ~doc ~line ~pos in
let result = LSP.json_of_goals goals ~logs in
Expand Down

0 comments on commit d926581

Please sign in to comment.