Skip to content

Commit

Permalink
Fix (respect) most end positions for diagnostics.
Browse files Browse the repository at this point in the history
Parallels https://github.com/leanprover/vscode-lean/blob/9a5f32602a5089fe9985df631f1b24aa44965063/src/diagnostics.ts#L67-L75
meaning we now handle the first two cases of leanprover-community/lean#744 (comment).

The last one is where end_pos is undefined, and what vscode does is
instead use a word range -- we can implement that from within lean.nvim.

Refs: leanprover-community/lean#744
  • Loading branch information
Julian committed Jul 16, 2022
1 parent e79dd09 commit bca7556
Showing 1 changed file with 7 additions and 2 deletions.
9 changes: 7 additions & 2 deletions lean-language-server/src/index.ts
Original file line number Diff line number Diff line change
Expand Up @@ -117,8 +117,13 @@ server.allMessages.on((messages) => {
}

for (const message of messages.msgs) {
const line = Math.max(message.pos_line - 1, 0);
const range = Range.create(line, message.pos_col, line, message.pos_col);
const start_line = Math.max(message.pos_line - 1, 0);
const end_line = Math.max(message.end_pos_line - 1, 0);
const start_pos = Position.create(start_line, message.pos_col)
const end_pos = message.end_pos_col !== undefined
? Position.create(end_line, message.end_pos_col)
: start_pos
const range = Range.create(start_pos, end_pos);
const diagnostics = diagnosticMap.get(URI.file(message.file_name).toString());
if (diagnostics) {
diagnostics.push({
Expand Down

0 comments on commit bca7556

Please sign in to comment.