mirror of
https://github.com/ilyakooo0/helix.git
synced 2024-08-17 03:50:21 +03:00
Add support for Agda (#8285)
* agda language support (wip) * improve highlights * disable agda-language-server * minor addendum to documentation * cargo xtask docgen * oh i can just do this neat * minor comment cleanup * upstream updated * imports: missed a spot --------- Co-authored-by: Michael Davis <mcarsondavis@gmail.com>
This commit is contained in:
parent
914c83420b
commit
c56cd6ee8b
@ -1,5 +1,6 @@
|
||||
| Language | Syntax Highlighting | Treesitter Textobjects | Auto Indent | Default LSP |
|
||||
| --- | --- | --- | --- | --- |
|
||||
| agda | ✓ | | | |
|
||||
| astro | ✓ | | | |
|
||||
| awk | ✓ | ✓ | | `awk-language-server` |
|
||||
| bash | ✓ | ✓ | ✓ | `bash-language-server` |
|
||||
|
@ -36,6 +36,7 @@ ## Queries
|
||||
3. Refer to the
|
||||
[tree-sitter website](https://tree-sitter.github.io/tree-sitter/syntax-highlighting#queries)
|
||||
for more information on writing queries.
|
||||
4. A list of highlight captures can be found [on the themes page](https://docs.helix-editor.com/themes.html#scopes).
|
||||
|
||||
> 💡 In Helix, the first matching query takes precedence when evaluating
|
||||
> queries, which is different from other editors such as Neovim where the last
|
||||
@ -51,3 +52,4 @@ ## Common issues
|
||||
grammars.
|
||||
- If a parser is causing a segfault, or you want to remove it, make sure to
|
||||
remove the compiled parser located at `runtime/grammars/<name>.so`.
|
||||
- If you are attempting to add queries and Helix is unable to locate them, ensure that the environment variable `HELIX_RUNTIME` is set to the location of the `runtime` folder you're developing in.
|
||||
|
@ -3,6 +3,7 @@
|
||||
|
||||
[language-server]
|
||||
|
||||
als = { command = "als" }
|
||||
awk-language-server = { command = "awk-language-server" }
|
||||
bash-language-server = { command = "bash-language-server", args = ["start"] }
|
||||
bass = { command = "bass", args = ["--lsp"] }
|
||||
@ -2920,6 +2921,32 @@ file-types = ["gmi"]
|
||||
name = "gemini"
|
||||
source = { git = "https://git.sr.ht/~nbsp/tree-sitter-gemini", rev = "3cc5e4bdf572d5df4277fc2e54d6299bd59a54b3" }
|
||||
|
||||
[[language]]
|
||||
name = "agda"
|
||||
scope = "source.agda"
|
||||
injection-regex = "agda"
|
||||
file-types = ["agda"]
|
||||
roots = []
|
||||
comment-token = "--"
|
||||
# language-servers = [ "als" ]
|
||||
# the agda language server is of questionable functionality.
|
||||
auto-format = false
|
||||
indent = { tab-width = 2, unit = " " }
|
||||
|
||||
[language.auto-pairs]
|
||||
'"' = '"'
|
||||
"'" = "'"
|
||||
'{' = '}'
|
||||
'(' = ')'
|
||||
'[' = ']'
|
||||
|
||||
# [language.debugger]
|
||||
# ?? can this be used for proof assistant support? explore
|
||||
|
||||
[[grammar]]
|
||||
name = "agda"
|
||||
source = { git = "https://github.com/tree-sitter/tree-sitter-agda", rev = "c21c3a0f996363ed17b8ac99d827fe5a4821f217" }
|
||||
|
||||
[[language]]
|
||||
name = "templ"
|
||||
scope = "source.templ"
|
||||
|
124
runtime/queries/agda/highlights.scm
Normal file
124
runtime/queries/agda/highlights.scm
Normal file
@ -0,0 +1,124 @@
|
||||
;; Punctuation
|
||||
[ "." ";" ":"] @punctuation.delimiter
|
||||
[ "(" ")" "{" "}" ] @punctuation.bracket
|
||||
|
||||
;; Constants
|
||||
(integer) @constant.numeric.integer
|
||||
; (float) @constant.numeric.float
|
||||
(literal) @string
|
||||
|
||||
;; Pragmas and comments
|
||||
(comment) @comment
|
||||
(pragma) @attribute
|
||||
(macro) @function.macro
|
||||
|
||||
;; Imports
|
||||
(module_name) @namespace
|
||||
(import_directive (id) @namespace)
|
||||
[(module) (import) (open)] @keyword.control.import
|
||||
|
||||
;; Types
|
||||
(typed_binding (expr) @type)
|
||||
(record (expr) @type)
|
||||
(data (expr) @type)
|
||||
(signature (expr) @type)
|
||||
(function (rhs (expr) @type))
|
||||
; todo: these are too general. ideally, any nested (atom)
|
||||
; https://github.com/tree-sitter/tree-sitter/issues/880
|
||||
|
||||
;; Variables
|
||||
(untyped_binding (atom) @variable)
|
||||
(typed_binding (atom) @variable)
|
||||
(field_name) @variable.other.member
|
||||
|
||||
;; Functions
|
||||
(function_name) @function
|
||||
;(function (lhs
|
||||
; . (atom) @function
|
||||
; (atom) @variable.parameter))
|
||||
; todo: currently fails to parse, upstream tree-sitter bug
|
||||
|
||||
;; Data
|
||||
[(data_name) (record_name)] @constructor
|
||||
((atom) @constant.builtin.boolean
|
||||
(#any-of? @constant.builtin.boolean "true" "false" "True" "False"))
|
||||
|
||||
"Set" @type.builtin
|
||||
|
||||
; postulate
|
||||
; type_signature
|
||||
; pattern
|
||||
; id
|
||||
; bid
|
||||
; typed_binding
|
||||
; primitive
|
||||
; private
|
||||
; record_signature
|
||||
; record_assignments
|
||||
; field_assignment
|
||||
; module_assignment
|
||||
; renaming
|
||||
; import_directive
|
||||
; lambda
|
||||
; let
|
||||
; instance
|
||||
; generalize
|
||||
; record
|
||||
; fields
|
||||
; syntax
|
||||
; hole_name
|
||||
; data_signature
|
||||
|
||||
;; Keywords
|
||||
[
|
||||
"where"
|
||||
"data"
|
||||
"rewrite"
|
||||
"postulate"
|
||||
"public"
|
||||
"private"
|
||||
"tactic"
|
||||
"Prop"
|
||||
"quote"
|
||||
"renaming"
|
||||
"in"
|
||||
"hiding"
|
||||
"constructor"
|
||||
"abstract"
|
||||
"let"
|
||||
"field"
|
||||
"mutual"
|
||||
"infix"
|
||||
"infixl"
|
||||
"infixr"
|
||||
"record"
|
||||
"overlap"
|
||||
"instance"
|
||||
"do"
|
||||
] @keyword
|
||||
|
||||
[
|
||||
"="
|
||||
] @operator
|
||||
|
||||
; = | -> : ? \ .. ... λ ∀ →
|
||||
; (_LAMBDA) (_FORALL) (_ARROW)
|
||||
; "coinductive"
|
||||
; "eta-equality"
|
||||
; "field"
|
||||
; "inductive"
|
||||
; "interleaved"
|
||||
; "macro"
|
||||
; "no-eta-equality"
|
||||
; "pattern"
|
||||
; "primitive"
|
||||
; "quoteTerm"
|
||||
; "rewrite"
|
||||
; "syntax"
|
||||
; "unquote"
|
||||
; "unquoteDecl"
|
||||
; "unquoteDef"
|
||||
; "using"
|
||||
; "variable"
|
||||
; "with"
|
||||
|
Loading…
Reference in New Issue
Block a user