Skip to content

Fix error location reporting for required files in LP console #1499

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

Merged
fblanqui merged 10 commits into from
Sep 8, 2026
Merged

Fix error location reporting for required files in LP console #1499

Changes from 4 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
c921453
add position to syntactic errors in LP consol
Alidra Sep 1, 2026
48abf93
fix location when error occurs in a different file
Alidra Sep 1, 2026
2e735d4
add space between location and error message
Alidra Sep 1, 2026
027d8ab
use short position in terminal in case of syntactic error
Alidra Sep 1, 2026
c004468
Use color when displaying error messages in LP console
Alidra Sep 2, 2026
09483d7
refactoring for readability
Alidra Sep 2, 2026
b88e065
add comment to pure.ml
Alidra Sep 2, 2026
69abbc7
wip
Alidra Sep 3, 2026
c8b7ef1
minor refactoring
Alidra Sep 7, 2026
fd38d41
extract function format_error_msg
Alidra Sep 7, 2026
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
30 changes: 22 additions & 8 deletions src/lsp/lp_doc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,20 +132,26 @@ let process_cmd _file (nodes,st,dg,logs) cmd =

| Cmd_Error(loc, msg) ->
Comment thread
fblanqui marked this conversation as resolved.
Outdated
Comment thread
fblanqui marked this conversation as resolved.
Outdated
let nodes = { cmd; exec = false; goals = [] } :: nodes in
let cmd_loc, loc, diag, log = match cmd_loc, loc with
let cmd_loc, diag, log = match cmd_loc, loc with
Comment thread
fblanqui marked this conversation as resolved.
Outdated
Comment thread
fblanqui marked this conversation as resolved.
Outdated
Comment thread
fblanqui marked this conversation as resolved.
Outdated
| Some l, Some Some l' ->
if l.fname = l'.fname then
(* if error in the same file, use the precise location *)
Comment thread
fblanqui marked this conversation as resolved.
Outdated
Some l', Some l', msg, Pos.popt_to_string (Some l') ^ msg
Some l',
msg,
Pos.popt_to_string
~print_dirname:false
~print_fname:false
(Some l') ^ " " ^ msg
else
(* else, use the location of the command *)
Comment thread
fblanqui marked this conversation as resolved.
Outdated
cmd_loc, Some l', Pos.popt_to_string (Some l') ^ "\n" ^ msg
, Pos.popt_to_string (Some l') ^ "\n" ^ msg
cmd_loc,
Pos.popt_to_string (Some l') ^ "\n" ^ msg,
Pos.popt_to_string (Some l') ^ "\n" ^ msg
(* Otherwise,
cmd_loc doesn't change and loc is : option_default loc cmd_loc *)
Comment thread
fblanqui marked this conversation as resolved.
Outdated
| _, Some l' -> cmd_loc, l', msg, Pos.popt_to_string (l') ^ "\n" ^ msg
| _, None -> cmd_loc, cmd_loc, msg, msg in
nodes, st, (cmd_loc, 1, diag, None) :: dg, ((1, log), loc) :: logs
| _, Some l' -> cmd_loc, msg, Pos.popt_to_string (l') ^ "\n" ^ msg
Comment thread
fblanqui marked this conversation as resolved.
Outdated
Comment thread
fblanqui marked this conversation as resolved.
Outdated
| _, None -> cmd_loc, msg, msg in
nodes, st, (cmd_loc, 1, diag, None) :: dg, ((1, log), cmd_loc) :: logs

let new_doc ~uri ~version ~text =
let root, logs =
Expand Down Expand Up @@ -205,7 +211,15 @@ let check_text ~doc =
let logs, diags =
match error with
| None -> logs, diags
| Some(pos,msg) -> logs @ [((1, msg), Some pos)], diags @ [pos,1,msg,None]
| Some(pos,msg) ->
Comment thread
fblanqui marked this conversation as resolved.
Outdated
logs @ [
((1,
(Pos.popt_to_string
~print_dirname:false
~print_fname:false
(Some pos) ^ ": " ^ msg)),
Some pos)],
diags @ [pos,1,msg,None]
in
let map = Pure.rangemap cmds in
let doc = { doc with nodes; final=Some(final); map; logs } in
Expand Down