-
Notifications
You must be signed in to change notification settings - Fork 23
/
lsp.lua
54 lines (49 loc) · 1.73 KB
/
lsp.lua
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
local M = { handlers = {} }
local function position_params()
-- Shift forward by 1, since in vim it's easier to reach word
-- boundaries in normal mode.
local params = vim.lsp.util.make_position_params()
params.position.character = params.position.character + 1
return params
end
function M.enable(opts)
opts.commands = vim.tbl_extend("keep", opts.commands or {}, {
LeanPlainGoal = {
function() vim.lsp.buf_request(0, "$/lean/plainGoal", position_params()) end;
description = "Describe the current tactic state."
};
LeanPlainTermGoal = {
function() vim.lsp.buf_request(0, "$/lean/plainTermGoal", position_params()) end;
description = "Describe the expected type of the current term."
};
})
opts.handlers = vim.tbl_extend("keep", opts.handlers or {}, {
["$/lean/plainGoal"] = M.handlers.plain_goal_handler;
["$/lean/plainTermGoal"] = M.handlers.plain_term_goal_handler;
})
require('lspconfig').leanls.setup(opts)
end
function M.handlers.plain_goal_handler (_, method, result, _, _, config)
config = config or {}
config.focus_id = method
if not (result and result.rendered) then
return
end
local markdown_lines = vim.lsp.util.convert_input_to_markdown_lines(result.rendered)
markdown_lines = vim.lsp.util.trim_empty_lines(markdown_lines)
if vim.tbl_isempty(markdown_lines) then
return
end
return vim.lsp.util.open_floating_preview(markdown_lines, "markdown", config)
end
function M.handlers.plain_term_goal_handler (_, method, result, _, _, config)
config = config or {}
config.focus_id = method
if not (result and result.goal) then
return
end
return vim.lsp.util.open_floating_preview(
vim.split(result.goal, '\n'), "leaninfo", config
)
end
return M