aboutsummaryrefslogtreecommitdiff
path: root/runtime/queries/agda
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/queries/agda')
-rw-r--r--runtime/queries/agda/highlights.scm124
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"
+