@@ -0,0 +1,124 @@
1+;; Punctuation
2+[ "." ";" ":"] @punctuation.delimiter
3+[ "(" ")" "{" "}" ] @punctuation.bracket
4+
5+;; Constants
6+(integer) @constant.numeric.integer
7+; (float) @constant.numeric.float
8+(literal) @string
9+
10+;; Pragmas and comments
11+(comment) @comment
12+(pragma) @attribute
13+(macro) @function.macro
14+
15+;; Imports
16+(module_name) @namespace
17+(import_directive (id) @namespace)
18+[(module) (import) (open)] @keyword.control.import
19+
20+;; Types
21+(typed_binding (expr) @type)
22+(record (expr) @type)
23+(data (expr) @type)
24+(signature (expr) @type)
25+(function (rhs (expr) @type))
26+; todo: these are too general. ideally, any nested (atom)
27+; https://github.com/tree-sitter/tree-sitter/issues/880
28+
29+;; Variables
30+(untyped_binding (atom) @variable)
31+(typed_binding (atom) @variable)
32+(field_name) @variable.other.member
33+
34+;; Functions
35+(function_name) @function
36+;(function (lhs
37+; . (atom) @function
38+; (atom) @variable.parameter))
39+; todo: currently fails to parse, upstream tree-sitter bug
40+
41+;; Data
42+[(data_name) (record_name)] @constructor
43+((atom) @constant.builtin.boolean
44+ (#any-of? @constant.builtin.boolean "true" "false" "True" "False"))
45+
46+"Set" @type.builtin
47+
48+; postulate
49+; type_signature
50+; pattern
51+; id
52+; bid
53+; typed_binding
54+; primitive
55+; private
56+; record_signature
57+; record_assignments
58+; field_assignment
59+; module_assignment
60+; renaming
61+; import_directive
62+; lambda
63+; let
64+; instance
65+; generalize
66+; record
67+; fields
68+; syntax
69+; hole_name
70+; data_signature
71+
72+;; Keywords
73+[
74+ "where"
75+ "data"
76+ "rewrite"
77+ "postulate"
78+ "public"
79+ "private"
80+ "tactic"
81+ "Prop"
82+ "quote"
83+ "renaming"
84+ "in"
85+ "hiding"
86+ "constructor"
87+ "abstract"
88+ "let"
89+ "field"
90+ "mutual"
91+ "infix"
92+ "infixl"
93+ "infixr"
94+ "record"
95+ "overlap"
96+ "instance"
97+ "do"
98+] @keyword
99+
100+[
101+ "="
102+] @operator
103+
104+; = | -> : ? \ .. ... λ ∀ →
105+; (_LAMBDA) (_FORALL) (_ARROW)
106+; "coinductive"
107+; "eta-equality"
108+; "field"
109+; "inductive"
110+; "interleaved"
111+; "macro"
112+; "no-eta-equality"
113+; "pattern"
114+; "primitive"
115+; "quoteTerm"
116+; "rewrite"
117+; "syntax"
118+; "unquote"
119+; "unquoteDecl"
120+; "unquoteDef"
121+; "using"
122+; "variable"
123+; "with"
124+