74 lines
2.4 KiB
VimL
74 lines
2.4 KiB
VimL
|
set isk+=-,#
|
|||
|
|
|
|||
|
|
|
|||
|
|
syn match quoxDelim /[\[\](){};]/
|
|||
|
|
syn match quoxDelim /\<_\>/
|
|||
|
|
hi def link quoxDelim Delimiter
|
|||
|
|
|
|||
|
|
" [todo] don't match these inside longer symbols!!
|
|||
|
|
syn match quoxSymbol /⇒\|=>\?\|∷\|::\?\|,/
|
|||
|
|
syn keyword quoxSymbol λ fun comp
|
|||
|
|
syn match quoxSymbol /\%(\<\%(δ\|dfun\)\>\|@\)\s*/ nextgroup=quoxDimension
|
|||
|
|
syn match quoxSymbol /\<coe\>\s*/ nextgroup=quoxTypeLine
|
|||
|
|
hi def link quoxSymbol Keyword
|
|||
|
|
|
|||
|
|
syn match quoxTypeLine /(/ contained nextgroup=quoxDimension
|
|||
|
|
hi link quoxTypeLine quoxDelim
|
|||
|
|
|
|||
|
|
syn keyword quoxBuiltinType String Nat IOState Type
|
|||
|
|
syn match quoxBuiltinType /×\|\*\*\|≡\|==\|→\|->\|\k\@<!ℕ\k\@!/
|
|||
|
|
syn match quoxBuiltinType /★/
|
|||
|
|
syn match quoxBuiltinType /\<Eq\>\s*/ nextgroup=quoxTypeLine
|
|||
|
|
hi def link quoxBuiltinType Type
|
|||
|
|
|
|||
|
|
syn keyword quoxBuiltinVal fst snd
|
|||
|
|
hi def link quoxBuiltinVal Function
|
|||
|
|
|
|||
|
|
syn match quoxNat /\<\d\%(\%(\d\|_\)*\d\)\?\>/
|
|||
|
|
syn match quoxNat /\c\<0x\x\%(\%(\x\|_\)*\x\)\?\>/
|
|||
|
|
hi def link quoxNat Number
|
|||
|
|
|
|||
|
|
syn region quoxString start=+"+ end=+"+ skip=+\\"+ contains=quoxCharEsc
|
|||
|
|
hi def link quoxString String
|
|||
|
|
|
|||
|
|
syn match quoxTag /'\k\+/
|
|||
|
|
syn region quoxTag start=+'"+ end=+"+ skip=+\\"+ contains=quoxCharEsc
|
|||
|
|
hi def link quoxTag Constant
|
|||
|
|
|
|||
|
|
syn match quoxCharEsc /\\\%(\\\|"\|x\x\+;\|[nt]\)/ contained
|
|||
|
|
hi def link quoxCharEsc SpecialChar
|
|||
|
|
|
|||
|
|
syn match quoxQty /\<[01#ω]\./
|
|||
|
|
hi def link quoxQty Special
|
|||
|
|
|
|||
|
|
syn match quoxDef /\<\%(def\|postulate\)[01#ω]\?\>/ contains=quoxQtySuffix
|
|||
|
|
syn match quoxQtySuffix /[01#ω]\>/ contained
|
|||
|
|
hi def link quoxDef Label
|
|||
|
|
hi def link quoxQtySuffix quoxQty
|
|||
|
|
|
|||
|
|
syn keyword quoxNamespace namespace
|
|||
|
|
hi def link quoxNamespace Type
|
|||
|
|
|
|||
|
|
syn match quoxCase /\<case[01#ω]\?\>/ contains=quoxQtySuffix
|
|||
|
|
syn keyword quoxCase return of
|
|||
|
|
hi def link quoxCase Conditional
|
|||
|
|
|
|||
|
|
syn match quoxDimension /\%([𝑖𝑗𝑘𝑙]\|\k\)\+/ contained
|
|||
|
|
hi def link quoxDimension PreProc
|
|||
|
|
|
|||
|
|
syn region quoxComment start=+{-+ end=+-}+ contains=quoxComment
|
|||
|
|
syn match quoxComment /--.*$/
|
|||
|
|
hi def link quoxComment Comment
|
|||
|
|
|
|||
|
|
syn keyword quoxLoad load
|
|||
|
|
hi def link quoxLoad Include
|
|||
|
|
|
|||
|
|
syn region quoxAttr matchgroup=quoxDelim start=+#\[+ end=+\]+ contains=TOP
|
|||
|
|
syn region quoxAttrBrack start=+\[+ end=+\]+ matchgroup=quoxDelim contained containedin=quoxAttr
|
|||
|
|
syn keyword quoxAttrName fail main compile-scheme contained containedin=quoxAttr
|
|||
|
|
hi def link quoxAttrName PreProc
|
|||
|
|
|
|||
|
|
syn match quoxDisplace /[⁰¹²³⁴⁵⁶⁷⁸⁹]\+/
|
|||
|
|
syn match quoxDisplace /\^\d\+/
|
|||
|
|
hi def link quoxDisplace Special
|