aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitmodules4
-rw-r--r--book/src/generated/lang-support.md1
m---------helix-syntax/languages/tree-sitter-lean0
-rw-r--r--languages.toml11
-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
8 files changed, 255 insertions, 0 deletions
diff --git a/.gitmodules b/.gitmodules
index 3442652a..1ccbe43b 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -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
diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md
index 87347819..fce14846 100644
--- a/book/src/generated/lang-support.md
+++ b/book/src/generated/lang-support.md
@@ -24,6 +24,7 @@
| json | ✓ | | ✓ | |
| julia | ✓ | | | `julia` |
| latex | ✓ | | | |
+| lean | ✓ | | | `lean` |
| ledger | ✓ | | | |
| llvm | ✓ | ✓ | ✓ | |
| llvm-mir | ✓ | ✓ | ✓ | |
diff --git a/helix-syntax/languages/tree-sitter-lean b/helix-syntax/languages/tree-sitter-lean
new file mode 160000
+Subproject d98426109258b266e1e92358c5f11716d2e8f63
diff --git a/languages.toml b/languages.toml
index af15c654..2896dd32 100644
--- a/languages.toml
+++ b/languages.toml
@@ -242,6 +242,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"
injection-regex = "julia"
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