mirror of
https://github.com/ilyakooo0/helix.git
synced 2024-08-17 03:50:21 +03:00
feat(languages): Lean experimental tree-sitter-lean (#1422)
* Add experimental tree-sitter-lean * Run docgen * Copy over the queries from lean.nvim * Update .gitmodules Co-authored-by: Ivan Tham <pickfire@riseup.net> * Update lean highlights and run docgen * Update runtime/queries/lean/injections.scm Co-authored-by: Michael Davis <michael.davis@nfiindustries.com> * Lean: Move variable matcher to bottom * Update runtime/queries/lean/locals.scm Co-authored-by: Michael Davis <michael.davis@nfiindustries.com> Co-authored-by: Ivan Tham <pickfire@riseup.net> Co-authored-by: Michael Davis <michael.davis@nfiindustries.com>
This commit is contained in:
parent
e7eab95b94
commit
8ea5742b08
4
.gitmodules
vendored
4
.gitmodules
vendored
@ -190,6 +190,10 @@
|
||||
path = helix-syntax/languages/tree-sitter-git-rebase
|
||||
url = https://github.com/the-mikedavis/tree-sitter-git-rebase.git
|
||||
shallow = true
|
||||
[submodule "helix-syntax/languages/tree-sitter-lean"]
|
||||
path = helix-syntax/languages/tree-sitter-lean
|
||||
url = https://github.com/Julian/tree-sitter-lean
|
||||
shallow = true
|
||||
[submodule "helix-syntax/languages/tree-sitter-regex"]
|
||||
path = helix-syntax/languages/tree-sitter-regex
|
||||
url = https://github.com/tree-sitter/tree-sitter-regex.git
|
||||
|
@ -24,6 +24,7 @@
|
||||
| json | ✓ | | ✓ | |
|
||||
| julia | ✓ | | | `julia` |
|
||||
| latex | ✓ | | | |
|
||||
| lean | ✓ | | | `lean` |
|
||||
| ledger | ✓ | | | |
|
||||
| llvm | ✓ | ✓ | ✓ | |
|
||||
| llvm-mir | ✓ | ✓ | ✓ | |
|
||||
|
1
helix-syntax/languages/tree-sitter-lean
Submodule
1
helix-syntax/languages/tree-sitter-lean
Submodule
@ -0,0 +1 @@
|
||||
Subproject commit d98426109258b266e1e92358c5f11716d2e8f638
|
@ -241,6 +241,17 @@ comment-token = "%"
|
||||
|
||||
indent = { tab-width = 4, unit = "\t" }
|
||||
|
||||
[[language]]
|
||||
name = "lean"
|
||||
scope = "source.lean"
|
||||
injection-regex = "lean"
|
||||
file-types = ["lean"]
|
||||
roots = [ "lakefile.lean" ]
|
||||
comment-token = "--"
|
||||
language-server = { command = "lean", args = [ "--server" ] }
|
||||
|
||||
indent = { tab-width = 2, unit = " " }
|
||||
|
||||
[[language]]
|
||||
name = "julia"
|
||||
scope = "source.julia"
|
||||
|
15
runtime/queries/lean/folds.scm
Normal file
15
runtime/queries/lean/folds.scm
Normal file
@ -0,0 +1,15 @@
|
||||
[
|
||||
(namespace)
|
||||
(section)
|
||||
|
||||
(instance)
|
||||
(def)
|
||||
(theorem)
|
||||
(example)
|
||||
|
||||
(product)
|
||||
(array)
|
||||
(list)
|
||||
|
||||
(string)
|
||||
] @fold
|
217
runtime/queries/lean/highlights.scm
Normal file
217
runtime/queries/lean/highlights.scm
Normal file
@ -0,0 +1,217 @@
|
||||
(open
|
||||
namespace: (identifier) @namespace)
|
||||
(namespace
|
||||
name: (identifier) @namespace)
|
||||
(section
|
||||
name: (identifier) @namespace)
|
||||
|
||||
;; Identifier naming conventions
|
||||
((identifier) @type
|
||||
(#match? @type "^[A-Z]"))
|
||||
|
||||
(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)
|
||||
|
||||
(proj
|
||||
name: (identifier) @field)
|
||||
|
||||
(binders
|
||||
type: (identifier) @type)
|
||||
|
||||
["if" "then" "else"] @keyword.control.conditional
|
||||
|
||||
["for" "in" "do"] @keyword.control.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_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) @constant.numeric.integer
|
||||
(float) @constant.numeric.float
|
||||
|
||||
(comment) @comment
|
||||
(char) @character
|
||||
(string) @string
|
||||
(interpolated_string) @string
|
||||
; (escape_sequence) @string.escape
|
||||
|
||||
; Reset highlighing in string interpolation
|
||||
(interpolation) @none
|
||||
|
||||
(interpolation
|
||||
"{" @punctuation.special
|
||||
"}" @punctuation.special)
|
||||
|
||||
["(" ")" "[" "]" "{" "}" "⟨" "⟩"] @punctuation.bracket
|
||||
|
||||
["|" "," "." ":" ";"] @punctuation.delimiter
|
||||
|
||||
(sorry) @error
|
||||
|
||||
;; Error
|
||||
(ERROR) @error
|
||||
|
||||
; Variables
|
||||
(identifier) @variable
|
2
runtime/queries/lean/injections.scm
Normal file
2
runtime/queries/lean/injections.scm
Normal file
@ -0,0 +1,2 @@
|
||||
((comment) @injection.content
|
||||
(#set! injection.language "markdown"))
|
5
runtime/queries/lean/locals.scm
Normal file
5
runtime/queries/lean/locals.scm
Normal file
@ -0,0 +1,5 @@
|
||||
[
|
||||
(module)
|
||||
(namespace)
|
||||
(section)
|
||||
] @local.scope
|
Loading…
Reference in New Issue
Block a user