helix-mirror/runtime/queries/agda/highlights.scm
JJ c56cd6ee8b
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>
2023-12-16 05:29:26 +01:00

125 lines
2.0 KiB
Scheme

;; 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"