Fix error location reporting for required files in LP console - #1499
Fix error location reporting for required files in LP console#1499Alidra wants to merge 8 commits into
Conversation
| | Cmd_Error(loc, msg) -> | ||
| 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 |
There was a problem hiding this comment.
diag should be renamed into diag_msg as it is not a diagnostic but a message.
Idem for log which should be renamed into log_msg.
In addition, to better understand the code, I also propose to rename cmd_loc into loc:
let loc, diag_msg, log_msg =
match cmd_loc, err_loc with
...
in
nodes, st, (loc, 1, diag_msg, None) :: dg, ((1, log_msg), loc) :: logs
| @@ -132,20 +132,26 @@ let process_cmd _file (nodes,st,dg,logs) cmd = | |||
|
|
|||
| | Cmd_Error(loc, msg) -> | |||
There was a problem hiding this comment.
please rename loc and msg into err_loc and err_msg respectively to understand the code more easily
| let cmd_loc, diag, log = match cmd_loc, loc with | ||
| | Some l, Some Some l' -> | ||
| if l.fname = l'.fname then | ||
| (* if error in the same file, use the precise location *) |
There was a problem hiding this comment.
if the error is in the same file as the command, we set the diag/log position to the error position and add the error position in the log message
| ~print_fname:false | ||
| (Some l') ^ " " ^ msg | ||
| else | ||
| (* else, use the location of the command *) |
There was a problem hiding this comment.
otherwise we set the diag/log position to the command position and add the error position to both the diag and log messages
| 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 *) |
There was a problem hiding this comment.
this comment is no longer up to date and should be removed
| @@ -132,20 +132,26 @@ let process_cmd _file (nodes,st,dg,logs) cmd = | |||
|
|
|||
| | Cmd_Error(loc, msg) -> | |||
There was a problem hiding this comment.
Could you please add also a comment in pure.mli to explain why Cmd_Error takes a popt option as argument (instead of just a popt) by referring to the comment given in error.ml (Cmd_Error inherits this from Fatal)?
| | Cmd_Error(loc, msg) -> | ||
| 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 |
There was a problem hiding this comment.
Isn't it the case that cmd_loc is never equal to None? If so, it would be nice to add:
| None, _ -> assert false
| | Cmd_Error(loc, msg) -> | ||
| 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 |
There was a problem hiding this comment.
Similarly, isn't it the case that err_loc is never equal to None? If so, it would be nice to add:
| _, None -> assert false
| | _, 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 |
There was a problem hiding this comment.
Please remove parentheses around l'.
| | _, 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 |
There was a problem hiding this comment.
Isn't the case that we always have l'=None here? If so, it would be better to write:
| Some _, Some None ->
(* error with no position *)
cmd_loc, msg, Pos.popt_to_string l' ^ "\n" ^ msg
It would be interesting to later investigate if this may actually happen.
2 participants
Summary
This PR fixes :
-1 The location is displayed in the LP console when a syntax error occurs (issue #1456)
-2 Errors are displayed in Red color and location is put between bracket (issue #1405)
-3 When an LP file requires another file and the error originates in the required file, the location of the
require opencommand is used so that when the "requiring" file is executed the error is displayed in the terminal when the user reaches the require command (issue #1498)Changes