mirror of
https://github.com/ilyakooo0/helix.git
synced 2024-11-28 21:20:23 +03:00
8ea5742b08
* 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>
218 lines
2.5 KiB
Scheme
218 lines
2.5 KiB
Scheme
(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
|