From c56cd6ee8b9312a620d4fc38eea90a49613f5d72 Mon Sep 17 00:00:00 2001
From: JJ <git@toki.la>
Date: Fri, 15 Dec 2023 20:29:26 -0800
Subject: [PATCH] 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>
---
 book/src/generated/lang-support.md  |   1 +
 book/src/guides/adding_languages.md |   2 +
 languages.toml                      |  27 ++++++
 runtime/queries/agda/highlights.scm | 124 ++++++++++++++++++++++++++++
 4 files changed, 154 insertions(+)
 create mode 100644 runtime/queries/agda/highlights.scm

diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md
index 1fad1017e..0ec8f5bad 100644
--- a/book/src/generated/lang-support.md
+++ b/book/src/generated/lang-support.md
@@ -1,5 +1,6 @@
 | Language | Syntax Highlighting | Treesitter Textobjects | Auto Indent | Default LSP |
 | --- | --- | --- | --- | --- |
+| agda | ✓ |  |  |  |
 | astro | ✓ |  |  |  |
 | awk | ✓ | ✓ |  | `awk-language-server` |
 | bash | ✓ | ✓ | ✓ | `bash-language-server` |
diff --git a/book/src/guides/adding_languages.md b/book/src/guides/adding_languages.md
index 93ec013f5..0763a3c5c 100644
--- a/book/src/guides/adding_languages.md
+++ b/book/src/guides/adding_languages.md
@@ -36,6 +36,7 @@ below.
 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 @@ below.
   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.
diff --git a/languages.toml b/languages.toml
index e184c8934..d05180ef1 100644
--- a/languages.toml
+++ b/languages.toml
@@ -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"
diff --git a/runtime/queries/agda/highlights.scm b/runtime/queries/agda/highlights.scm
new file mode 100644
index 000000000..4ddf849d0
--- /dev/null
+++ b/runtime/queries/agda/highlights.scm
@@ -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"
+