Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix the list of messages to be displayed in terminal due to position error #1150

Merged
merged 9 commits into from
Nov 18, 2024
Merged

Fix the list of messages to be displayed in terminal due to position error #1150

Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
c51ba17
vscode: remove debugin message
Alidra Jul 17, 2024
5148f2b
vscode: set preserveFocus to true to prevent Goals panel from taking …
Alidra Jul 17, 2024
cfce47a
Merge branch 'Deducteam:master' into master
Alidra Sep 30, 2024
a63f1d6
vscode: release minor revision to bring Goals panel to front whithout…
Alidra Sep 30, 2024
d27c7d7
Merge branch 'Deducteam:master' into master
Alidra Oct 15, 2024
29f9c9c
Merge branch 'Deducteam:master' into master
Alidra Nov 2, 2024
ba37966
Merge branch 'Deducteam:master' into master
Alidra Nov 13, 2024
3fc1ac6
fix comparaison operator to correctly show messages in terminal
Alidra Nov 14, 2024
77e471d
move calculation of position to get_goals instead of do_goals to be c…
Alidra Nov 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 20 additions & 19 deletions src/lsp/lp_lsp.ml
View file
Open in desktop
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
Loading