diff options
| -rw-r--r-- | .gitmodules | 4 | ||||
| -rw-r--r-- | book/src/generated/lang-support.md | 1 | ||||
| m--------- | helix-syntax/languages/tree-sitter-lean | 0 | ||||
| -rw-r--r-- | languages.toml | 11 | ||||
| -rw-r--r-- | runtime/queries/lean/folds.scm | 15 | ||||
| -rw-r--r-- | runtime/queries/lean/highlights.scm | 217 | ||||
| -rw-r--r-- | runtime/queries/lean/injections.scm | 2 | ||||
| -rw-r--r-- | runtime/queries/lean/locals.scm | 5 |
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 |