diff options
author | JJ | 2023-11-01 04:33:05 +0000 |
---|---|---|
committer | JJ | 2023-11-01 04:33:05 +0000 |
commit | 9663740245e2c18e160f6563d2f114f59d27b7c9 (patch) | |
tree | 747339a20cbb18011a34259241b3bb3baed96eb3 /runtime/queries/agda | |
parent | a4394d502f8ee551660af5c8f04545cca349efb9 (diff) |
Add support for Agda, update default Nim LSP23.10.1
Diffstat (limited to 'runtime/queries/agda')
-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" + |