nvim: Add support for lean

Tree sitter queries are copied over from lean.nvim.
This commit is contained in:
Sanchayan Maity 2024-02-19 19:42:06 +05:30
parent 0678b968b5
commit 86747c619d
Signed by: sanchayanmaity
GPG key ID: 6F6A0609C12038F3
7 changed files with 262 additions and 0 deletions

View file

@ -0,0 +1,4 @@
local lsp_utils = require('lsp-utils')
local leanls_config = lsp_utils.leanls_config()
vim.lsp.start(leanls_config)

View file

@ -201,6 +201,20 @@ function M.hls_config()
} }
end end
function M.leanls_config()
local root_files = { 'lakefile.lean', 'lean-toolchain', 'leanpkg.toml' }
local root_directory = get_root_directory(root_files)
return {
name = "leanls",
cmd = { 'lake', 'serve', '--' },
capabilities = default_capabilities,
root_dir = root_directory,
filetypes = { 'lean' },
single_file_support = true,
}
end
function M.pursls_config() function M.pursls_config()
local root_files = { 'bower.json', 'psc-package.json', 'spago.dhall' } local root_files = { 'bower.json', 'psc-package.json', 'spago.dhall' }
local root_directory = get_root_directory(root_files) local root_directory = get_root_directory(root_files)

View file

@ -17,5 +17,13 @@ require'nvim-treesitter.configs'.setup {
}, },
} }
require "nvim-treesitter.parsers".get_parser_configs().lean = {
filetype = "lean",
install_info = {
url = "~/GitSources/tree-sitter-lean",
files = {"src/parser.c", "src/scanner.cc"},
},
}
vim.keymap.set('o', '<Leader>m', ':<C-U>lua require(\'tsht\').nodes()<CR>', { noremap=false, unique=true, silent=true }) vim.keymap.set('o', '<Leader>m', ':<C-U>lua require(\'tsht\').nodes()<CR>', { noremap=false, unique=true, silent=true })
vim.keymap.set('x', '<Leader>m', ':lua require(\'tsht\').nodes()<CR>' , { noremap=true , unique=true, silent=true }) vim.keymap.set('x', '<Leader>m', ':lua require(\'tsht\').nodes()<CR>' , { noremap=true , unique=true, silent=true })

View file

@ -0,0 +1,15 @@
[
(namespace)
(section)
(instance)
(def)
(theorem)
(example)
(product)
(array)
(list)
(string)
] @fold

View file

@ -0,0 +1,216 @@
(open
namespace: (identifier) @namespace)
(namespace
name: (identifier) @namespace)
(section
name: (identifier) @namespace)
(arrow) @type
(product) @type
;; Declarations
[
"abbrev"
"def"
"theorem"
"constant"
"instance"
"axiom"
"example"
"inductive"
"structure"
"class"
"deriving"
"section"
"namespace"
] @keyword
(attributes
(identifier) @function)
(abbrev
name: (identifier) @type)
(def
name: (identifier) @function)
(theorem
name: (identifier) @function)
(constant
name: (identifier) @type)
(instance
name: (identifier) @function)
(instance
type: (identifier) @type)
(axiom
name: (identifier) @function)
(structure
name: (identifier) @type)
(structure
extends: (identifier) @type)
(where_decl
type: (identifier) @type)
(implicit_binder
type: (identifier) @type)
(explicit_binder
type: (identifier) @type)
(proj
name: (identifier) @field)
(binders
type: (identifier) @type)
["if" "then" "else"] @conditional
["for" "in" "do"] @repeat
(import) @include
; Tokens
[
"!"
"$"
"%"
"&&"
"*"
"*>"
"+"
"++"
"-"
"/"
"::"
":="
"<"
"<$>"
"<*"
"<*>"
"<="
"<|"
"<|>"
"="
"=="
"=>"
">"
">"
">="
">>"
">>="
"@"
"^"
"|>"
"|>."
"||"
"←"
"→"
"↔"
"∘"
"∧"
""
"≠"
"≤"
"≥"
] @operator
[
"@&"
] @operator
[
"attribute"
"by"
"end"
"export"
"extends"
"fun"
"let"
"have"
"match"
"open"
"return"
"universe"
"variable"
"where"
"with"
"λ"
(hash_command)
(prelude)
(sorry)
] @keyword
[
"prefix"
"infix"
"infixl"
"infixr"
"postfix"
"notation"
"macro"
"macro_rules"
"syntax"
"elab"
"builtin_initialize"
] @keyword
[
"noncomputable"
"partial"
"private"
"protected"
"unsafe"
] @keyword
[
"apply"
"exact"
"rewrite"
"rw"
"simp"
(trivial)
] @keyword
[
"catch"
"finally"
"try"
] @exception
((apply
name: (identifier) @exception)
(#match? @exception "throw"))
[
"unless"
"mut"
] @keyword
[(true) (false)] @boolean
(number) @number
(float) @float
(comment) @comment
(char) @character
(string) @string
(interpolated_string) @string
(quoted_char) @string.escape
; Reset highlighing in string interpolation
(interpolation) @none
(interpolation
"{" @punctuation.special
"}" @punctuation.special)
["(" ")" "[" "]" "{" "}" "⟨" "⟩"] @punctuation.bracket
["|" "," "." ":" ";"] @punctuation.delimiter
(sorry) @error
;; Error
(ERROR) @error

View file

@ -0,0 +1,2 @@
((comment) @markdown
(#offset! @markdown 0 3 0 -2))

View file

@ -0,0 +1,3 @@
(module) @scope
(namespace) @scope
(section) @scope