2024-05-16 16:01:06 -04:00
|
|
|
|
if exists('b:current_syntax')
|
|
|
|
|
|
finish
|
|
|
|
|
|
endif
|
|
|
|
|
|
let b:current_syntax = 'quox'
|
2023-11-05 16:15:02 -05:00
|
|
|
|
|
2024-05-16 16:01:20 -04:00
|
|
|
|
setlocal iskeyword+=#
|
|
|
|
|
|
setlocal iskeyword+=-
|
|
|
|
|
|
setlocal iskeyword+='
|
2023-11-05 16:15:02 -05:00
|
|
|
|
|
|
|
|
|
|
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\)\?\>/
|
2024-05-16 16:02:08 -04:00
|
|
|
|
syn keyword quoxNat zero succ
|
2023-11-05 16:15:02 -05:00
|
|
|
|
hi def link quoxNat Number
|
|
|
|
|
|
|
|
|
|
|
|
syn region quoxString start=+"+ end=+"+ skip=+\\"+ contains=quoxCharEsc
|
|
|
|
|
|
hi def link quoxString String
|
|
|
|
|
|
|
2024-05-16 16:01:20 -04:00
|
|
|
|
syn match quoxTag /\<'\k\+/
|
|
|
|
|
|
syn region quoxTag start=+\<'"+ end=+"+ skip=+\\"+ contains=quoxCharEsc
|
2023-11-05 16:15:02 -05:00
|
|
|
|
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
|
