aboutsummaryrefslogtreecommitdiff
path: root/runtime/queries/lean
diff options
context:
space:
mode:
authorAnders Christiansen Sørby2022-01-17 14:05:17 +0000
committerGitHub2022-01-17 14:05:17 +0000
commit8ea5742b0899992cd7453c70a8a06cb76a703fdf (patch)
treef2bfef8caff17770525196a95113f07ff5cad65d /runtime/queries/lean
parente7eab95b943ff15396c5d512a9c95650ab98a902 (diff)
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>
Diffstat (limited to 'runtime/queries/lean')
-rw-r--r--runtime/queries/lean/folds.scm15
-rw-r--r--runtime/queries/lean/highlights.scm217
-rw-r--r--runtime/queries/lean/injections.scm2
-rw-r--r--runtime/queries/lean/locals.scm5
4 files changed, 239 insertions, 0 deletions
diff --git a/runtime/queries/lean/folds.scm b/runtime/queries/lean/folds.scm
new file mode 100644
index 00000000..2c2bbb33
--- /dev/null
+++ b/runtime/queries/lean/folds.scm
@@ -0,0 +1,15 @@
+[
+ (namespace)
+ (section)
+
+ (instance)
+ (def)
+ (theorem)
+ (example)
+
+ (product)
+ (array)
+ (list)
+
+ (string)
+] @fold
diff --git a/runtime/queries/lean/highlights.scm b/runtime/queries/lean/highlights.scm
new file mode 100644
index 00000000..a64feb1d
--- /dev/null
+++ b/runtime/queries/lean/highlights.scm
@@ -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
diff --git a/runtime/queries/lean/injections.scm b/runtime/queries/lean/injections.scm
new file mode 100644
index 00000000..030714f1
--- /dev/null
+++ b/runtime/queries/lean/injections.scm
@@ -0,0 +1,2 @@
+((comment) @injection.content
+ (#set! injection.language "markdown"))
diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm
new file mode 100644
index 00000000..dd6c2036
--- /dev/null
+++ b/runtime/queries/lean/locals.scm
@@ -0,0 +1,5 @@
+[
+ (module)
+ (namespace)
+ (section)
+] @local.scope