90 lines
2.2 KiB
VimL
90 lines
2.2 KiB
VimL
if exists('b:current_syntax')
|
|
finish
|
|
endif
|
|
let b:current_syntax = 'beluga'
|
|
|
|
setlocal iskeyword=@,48-57,63-64,a-z,A-Z,!,$,&,',*,+,_,/,=,-,~,#,^
|
|
setlocal comments=b:%,srn:%{,m:\ ,ern:}%
|
|
setlocal commentstring=%%s
|
|
|
|
syn match belArrowEtc /->\|=>\|→\|⇒\||-#\?\|⊢\|\<=\>\|:/
|
|
hi def link belArrowEtc Function
|
|
|
|
syn match belDelim /[()\]{}.;,]\|[#$]\?\[\|\<\/\>\||-\@!\|<\|-\@<!>/
|
|
hi def link belDelim Delimiter
|
|
|
|
syn match belComment /%.*$/
|
|
hi def link belComment Comment
|
|
|
|
syn region belBlockComment start='%{' end='}%' contains=belBlockComment
|
|
hi def link belBlockComment belComment
|
|
|
|
syn keyword belUnderscore _ #_ $_
|
|
hi def link belUnderscore Special
|
|
|
|
syn keyword belType type ctype
|
|
hi def link belType Typedef
|
|
|
|
syn match belPragma /\%(%\|\<--\)\%(coverage\|warncoverage\|nostrengthen\|infix\|prefix\|assoc\|name\|abbrev\|not\|open\)\>/
|
|
hi def link belPragma Special
|
|
|
|
syn keyword belDecl
|
|
\ LF inductive coinductive stratified proof schema rec and typedef
|
|
hi def link belDecl Structure
|
|
|
|
syn keyword belTotal total
|
|
hi def link belTotal Special
|
|
|
|
syn keyword belTrust trust
|
|
hi def link belTrust Underlined
|
|
|
|
syn match belSubstConst /\.\.\|\^/
|
|
hi def link belSubstConst Constant
|
|
|
|
syn keyword belIdBlock some block
|
|
hi def link belIdBlock Structure
|
|
|
|
syn keyword belModule module struct end
|
|
hi def link belModule Structure
|
|
|
|
syn match belQualName /\>::\</
|
|
hi def link belQualName Normal
|
|
|
|
syn match belVarVar /#\k\+/
|
|
hi def link belVarVar Constant
|
|
|
|
syn match belSubstVar /\$\k\+/
|
|
hi def link belSubstVar String
|
|
|
|
syn region belObjLam
|
|
\ matchgroup=belObjLamP start=/\\/ matchgroup=belArrowEtc end=/\./ transparent
|
|
hi def link belObjLamP Define
|
|
|
|
syn keyword belMetaLam fn mlam fun
|
|
hi def link belMetaLam Define
|
|
|
|
syn keyword belCase case of impossible
|
|
hi def link belCase Keyword
|
|
|
|
syn keyword belLet let in
|
|
hi def link belLet Keyword
|
|
|
|
syn match belSubBlock /\.\k\+\>/
|
|
hi def link belSubBlock Label
|
|
|
|
syn keyword belBoolType Bool
|
|
hi def link belBoolType Typedef
|
|
|
|
syn keyword belBool ttrue ffalse
|
|
hi def link belBool Boolean
|
|
|
|
syn keyword belIf if then else
|
|
hi def link belIf Keyword
|
|
|
|
syn match belugaError /<-\|←/
|
|
syn keyword belugaError prop
|
|
hi def link belugaError Error
|
|
|
|
syn match belugaHole /\<?\k*\>/
|
|
hi def link belugaHole Underlined
|