From 40c28ec3d739a4a551201bd7ad8c125c15e54dbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Sun, 2 Jan 2022 20:53:24 +0100 Subject: [PATCH 1/8] Add experimental tree-sitter-lean --- .gitmodules | 4 ++++ helix-syntax/languages/tree-sitter-lean | 1 + languages.toml | 11 +++++++++++ 3 files changed, 16 insertions(+) create mode 160000 helix-syntax/languages/tree-sitter-lean diff --git a/.gitmodules b/.gitmodules index 22f70c802655..f64922b43b1d 100644 --- a/.gitmodules +++ b/.gitmodules @@ -182,3 +182,7 @@ 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"] + shallow = true + path = helix-syntax/languages/tree-sitter-lean + url = https://github.com/Julian/tree-sitter-lean diff --git a/helix-syntax/languages/tree-sitter-lean b/helix-syntax/languages/tree-sitter-lean new file mode 160000 index 000000000000..d98426109258 --- /dev/null +++ b/helix-syntax/languages/tree-sitter-lean @@ -0,0 +1 @@ +Subproject commit d98426109258b266e1e92358c5f11716d2e8f638 diff --git a/languages.toml b/languages.toml index f088a3aaa5fa..5baf621c1dc5 100644 --- a/languages.toml +++ b/languages.toml @@ -240,6 +240,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" From 6bc6d781a4073ed86f565548bcef27879d074082 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Mon, 3 Jan 2022 13:57:36 +0100 Subject: [PATCH 2/8] Run docgen --- book/src/generated/lang-support.md | 1 + 1 file changed, 1 insertion(+) diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md index 09284d467b77..e4bce655e544 100644 --- a/book/src/generated/lang-support.md +++ b/book/src/generated/lang-support.md @@ -22,6 +22,7 @@ | json | ✓ | | ✓ | | | julia | ✓ | | | `julia` | | latex | ✓ | | | | +| lean | | | | `lean` | | ledger | ✓ | | | | | llvm | ✓ | ✓ | ✓ | | | lua | ✓ | | ✓ | | From 35b56e380b029039aae10b086fcd4d7159cd5389 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Tue, 4 Jan 2022 15:54:15 +0100 Subject: [PATCH 3/8] Copy over the queries from lean.nvim --- runtime/queries/lean/folds.scm | 15 ++ runtime/queries/lean/highlights.scm | 217 ++++++++++++++++++++++++++++ runtime/queries/lean/injections.scm | 2 + runtime/queries/lean/locals.scm | 3 + 4 files changed, 237 insertions(+) create mode 100644 runtime/queries/lean/folds.scm create mode 100644 runtime/queries/lean/highlights.scm create mode 100644 runtime/queries/lean/injections.scm create mode 100644 runtime/queries/lean/locals.scm diff --git a/runtime/queries/lean/folds.scm b/runtime/queries/lean/folds.scm new file mode 100644 index 000000000000..2c2bbb33ae23 --- /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 000000000000..9024e9fa79c0 --- /dev/null +++ b/runtime/queries/lean/highlights.scm @@ -0,0 +1,217 @@ +(open + namespace: (identifier) @namespace) +(namespace + name: (identifier) @namespace) +(section + name: (identifier) @namespace) + +; Variables +(identifier) @variable + +;; 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"] @conditional + +["for" "in" "do"] @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) @number +(float) @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 diff --git a/runtime/queries/lean/injections.scm b/runtime/queries/lean/injections.scm new file mode 100644 index 000000000000..50781594f661 --- /dev/null +++ b/runtime/queries/lean/injections.scm @@ -0,0 +1,2 @@ +((comment) @markdown + (#offset! @markdown 0 3 0 -2)) diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm new file mode 100644 index 000000000000..c3109e8387fb --- /dev/null +++ b/runtime/queries/lean/locals.scm @@ -0,0 +1,3 @@ +(module) @scope +(namespace) @scope +(section) @scope From 6d7ea9f8d1f068ac7188947bd77ed5f7739567cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Tue, 4 Jan 2022 16:28:48 +0100 Subject: [PATCH 4/8] Update .gitmodules Co-authored-by: Ivan Tham --- .gitmodules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index f64922b43b1d..928a79d372f1 100644 --- a/.gitmodules +++ b/.gitmodules @@ -183,6 +183,6 @@ url = https://github.com/the-mikedavis/tree-sitter-git-rebase.git shallow = true [submodule "helix-syntax/languages/tree-sitter-lean"] - shallow = true path = helix-syntax/languages/tree-sitter-lean url = https://github.com/Julian/tree-sitter-lean + shallow = true From a3c44085833429ead01b26592e6f456c32f8460a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Wed, 5 Jan 2022 15:57:23 +0100 Subject: [PATCH 5/8] Update lean highlights and run docgen --- book/src/generated/lang-support.md | 2 +- runtime/queries/lean/highlights.scm | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md index e4bce655e544..1ed395c287a1 100644 --- a/book/src/generated/lang-support.md +++ b/book/src/generated/lang-support.md @@ -22,7 +22,7 @@ | json | ✓ | | ✓ | | | julia | ✓ | | | `julia` | | latex | ✓ | | | | -| lean | | | | `lean` | +| lean | ✓ | | | `lean` | | ledger | ✓ | | | | | llvm | ✓ | ✓ | ✓ | | | lua | ✓ | | ✓ | | diff --git a/runtime/queries/lean/highlights.scm b/runtime/queries/lean/highlights.scm index 9024e9fa79c0..287442e5dd49 100644 --- a/runtime/queries/lean/highlights.scm +++ b/runtime/queries/lean/highlights.scm @@ -66,9 +66,9 @@ (binders type: (identifier) @type) -["if" "then" "else"] @conditional +["if" "then" "else"] @keyword.control.conditional -["for" "in" "do"] @repeat +["for" "in" "do"] @keyword.control.repeat (import) @include @@ -191,8 +191,8 @@ [(true) (false)] @boolean -(number) @number -(float) @float +(number) @constant.numeric.integer +(float) @constant.numeric.float (comment) @comment (char) @character From a4e96bd467e2eb3467bf7c1b31bdab987d60a500 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Thu, 13 Jan 2022 21:09:41 +0100 Subject: [PATCH 6/8] Update runtime/queries/lean/injections.scm Co-authored-by: Michael Davis --- runtime/queries/lean/injections.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/runtime/queries/lean/injections.scm b/runtime/queries/lean/injections.scm index 50781594f661..030714f1ce17 100644 --- a/runtime/queries/lean/injections.scm +++ b/runtime/queries/lean/injections.scm @@ -1,2 +1,2 @@ -((comment) @markdown - (#offset! @markdown 0 3 0 -2)) +((comment) @injection.content + (#set! injection.language "markdown")) From 6890c083f8918c4a3a29a2767c6fb2afb43a5f82 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Thu, 13 Jan 2022 21:18:41 +0100 Subject: [PATCH 7/8] Lean: Move variable matcher to bottom --- runtime/queries/lean/highlights.scm | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/runtime/queries/lean/highlights.scm b/runtime/queries/lean/highlights.scm index 287442e5dd49..a64feb1d390d 100644 --- a/runtime/queries/lean/highlights.scm +++ b/runtime/queries/lean/highlights.scm @@ -5,9 +5,6 @@ (section name: (identifier) @namespace) -; Variables -(identifier) @variable - ;; Identifier naming conventions ((identifier) @type (#match? @type "^[A-Z]")) @@ -215,3 +212,6 @@ ;; Error (ERROR) @error + +; Variables +(identifier) @variable From 47af837c33ccbe18c2c0a26c12c6e791298854c5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Thu, 13 Jan 2022 22:08:13 +0100 Subject: [PATCH 8/8] Update runtime/queries/lean/locals.scm Co-authored-by: Michael Davis --- runtime/queries/lean/locals.scm | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm index c3109e8387fb..dd6c203631bf 100644 --- a/runtime/queries/lean/locals.scm +++ b/runtime/queries/lean/locals.scm @@ -1,3 +1,5 @@ -(module) @scope -(namespace) @scope -(section) @scope +[ + (module) + (namespace) + (section) +] @local.scope