2020-06-11 23:22:29 -04:00
|
|
|
if exists('b:current_syntax')
|
|
|
|
finish
|
|
|
|
endif
|
2020-06-12 12:12:26 -04:00
|
|
|
let b:current_syntax = 'beluga'
|
2020-06-11 23:22:29 -04:00
|
|
|
|
2022-07-11 11:27:05 -04:00
|
|
|
setlocal iskeyword=@,48-57,63-64,a-z,A-Z,!,$,&,',*,+,_,/,=,-,~,#,^
|
2022-06-24 09:58:55 -04:00
|
|
|
setlocal comments=b:%,srn:%{,m:\ ,ern:}%
|
|
|
|
setlocal commentstring=%%s
|
2020-06-12 00:26:30 -04:00
|
|
|
|
2020-06-12 12:12:38 -04:00
|
|
|
syn match belArrowEtc /->\|=>\|→\|⇒\||-#\?\|⊢\|\<=\>\|:/
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belArrowEtc Function
|
|
|
|
|
2022-07-15 08:54:53 -04:00
|
|
|
syn match belDelim /[()\]{}.;,]\|[#$]\?\[\|\<\/\>\||-\@!\|<\|-\@<!>/
|
2020-06-12 13:53:46 -04:00
|
|
|
hi def link belDelim Delimiter
|
2020-06-12 00:26:30 -04:00
|
|
|
|
2022-07-15 08:54:57 -04:00
|
|
|
syn match belComment /%.*$/
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belComment Comment
|
|
|
|
|
|
|
|
syn region belBlockComment start='%{' end='}%' contains=belBlockComment
|
|
|
|
hi def link belBlockComment belComment
|
|
|
|
|
2020-06-12 02:08:54 -04:00
|
|
|
syn keyword belUnderscore _ #_ $_
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belUnderscore Special
|
|
|
|
|
2020-06-12 02:08:54 -04:00
|
|
|
syn keyword belType type ctype
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belType Typedef
|
|
|
|
|
|
|
|
syn match belPragma /\%(%\|\<--\)\%(coverage\|warncoverage\|nostrengthen\|infix\|prefix\|assoc\|name\|abbrev\|not\|open\)\>/
|
|
|
|
hi def link belPragma Special
|
|
|
|
|
2020-06-12 20:03:19 -04:00
|
|
|
syn keyword belDecl
|
|
|
|
\ LF inductive coinductive fun stratified proof schema rec and typedef
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belDecl Structure
|
|
|
|
|
|
|
|
syn keyword belTotal total
|
|
|
|
hi def link belTotal Special
|
|
|
|
|
|
|
|
syn keyword belTrust trust
|
|
|
|
hi def link belTrust Underlined
|
|
|
|
|
2020-06-12 13:53:59 -04:00
|
|
|
syn match belSubstConst /\.\.\|\^/
|
|
|
|
hi def link belSubstConst Constant
|
2020-06-12 00:26:30 -04:00
|
|
|
|
|
|
|
syn keyword belIdBlock some block
|
|
|
|
hi def link belIdBlock Structure
|
|
|
|
|
2020-06-12 13:54:15 -04:00
|
|
|
syn keyword belModule module struct end
|
|
|
|
hi def link belModule Structure
|
|
|
|
|
|
|
|
syn match belQualName /\>::\</
|
|
|
|
hi def link belQualName Normal
|
|
|
|
|
2020-06-12 02:08:54 -04:00
|
|
|
syn match belVarVar /#\k\+/
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belVarVar Constant
|
|
|
|
|
2020-06-12 02:08:54 -04:00
|
|
|
syn match belSubstVar /\$\k\+/
|
2020-06-12 00:26:30 -04:00
|
|
|
hi def link belSubstVar String
|
|
|
|
|
|
|
|
syn region belObjLam
|
|
|
|
\ matchgroup=belObjLamP start=/\\/ matchgroup=belArrowEtc end=/\./ transparent
|
|
|
|
hi def link belObjLamP Define
|
|
|
|
|
2022-06-24 10:17:19 -04:00
|
|
|
syn keyword belMetaLam fn mlam
|
2020-06-12 00:26:30 -04:00
|
|
|
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
|
2020-06-12 13:54:25 -04:00
|
|
|
|
2020-06-12 13:55:47 -04:00
|
|
|
syn match belugaError /<-\|←/
|
2020-06-12 13:54:25 -04:00
|
|
|
syn keyword belugaError prop
|
|
|
|
hi def link belugaError Error
|
2022-07-11 11:27:11 -04:00
|
|
|
|
|
|
|
syn match belugaHole /\<?\k*\>/
|
|
|
|
hi def link belugaHole Underlined
|