diff options
author | JJ | 2023-12-16 04:29:26 +0000 |
---|---|---|
committer | GitHub | 2023-12-16 04:29:26 +0000 |
commit | c56cd6ee8b9312a620d4fc38eea90a49613f5d72 (patch) | |
tree | ce90625c3fd89600368114697d7f9af0b7173d07 /runtime | |
parent | 914c83420b9901f596bf771ad5f20495de9a070c (diff) |
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>
Diffstat (limited to 'runtime')
-rw-r--r-- | runtime/queries/agda/highlights.scm | 124 |
1 files changed, 124 insertions, 0 deletions
diff --git a/runtime/queries/agda/highlights.scm b/runtime/queries/agda/highlights.scm new file mode 100644 index 00000000..4ddf849d --- /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" + |