aboutsummaryrefslogtreecommitdiff
path: root/runtime/queries/lean
diff options
context:
space:
mode:
authorBlaž Hrastnik2022-02-13 09:31:51 +0000
committerBlaž Hrastnik2022-02-13 09:31:51 +0000
commitbd549d8a20cce98e24c8653a4a86107c786cbaa3 (patch)
tree0780b58d41b6181e69023265cdb54517e2953778 /runtime/queries/lean
parent7ad8eaaef0b292f4be6c66298cea40d2b928e172 (diff)
parent7083b98a388b30e0b61caac9bf6ccc1d79eadf81 (diff)
Merge remote-tracking branch 'origin/master' into debug
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