Compare commits
6 Commits
3229be14f8
...
41766c5db6
Author | SHA1 | Date |
---|---|---|
rhiannon morris | 41766c5db6 | |
rhiannon morris | 9fae64707e | |
rhiannon morris | c3ec8631ae | |
rhiannon morris | 0c1cb6f77a | |
rhiannon morris | f58e67db1c | |
rhiannon morris | 6ae3479480 |
|
@ -10,10 +10,10 @@ setlocal commentstring=%%s
|
||||||
syn match belArrowEtc /->\|=>\|→\|⇒\||-#\?\|⊢\|\<=\>\|:/
|
syn match belArrowEtc /->\|=>\|→\|⇒\||-#\?\|⊢\|\<=\>\|:/
|
||||||
hi def link belArrowEtc Function
|
hi def link belArrowEtc Function
|
||||||
|
|
||||||
syn match belDelim /[()[\]{}.;,]\|\<\/\>\||-\@!\|<\|-\@<!>/
|
syn match belDelim /[()\]{}.;,]\|[#$]\?\[\|\<\/\>\||-\@!\|<\|-\@<!>/
|
||||||
hi def link belDelim Delimiter
|
hi def link belDelim Delimiter
|
||||||
|
|
||||||
syn match belComment /%\+\s.*$/
|
syn match belComment /%.*$/
|
||||||
hi def link belComment Comment
|
hi def link belComment Comment
|
||||||
|
|
||||||
syn region belBlockComment start='%{' end='}%' contains=belBlockComment
|
syn region belBlockComment start='%{' end='}%' contains=belBlockComment
|
||||||
|
@ -29,7 +29,7 @@ syn match belPragma /\%(%\|\<--\)\%(coverage\|warncoverage\|nostrengthen\|infix\
|
||||||
hi def link belPragma Special
|
hi def link belPragma Special
|
||||||
|
|
||||||
syn keyword belDecl
|
syn keyword belDecl
|
||||||
\ LF inductive coinductive fun stratified proof schema rec and typedef
|
\ LF inductive coinductive stratified proof schema rec and typedef
|
||||||
hi def link belDecl Structure
|
hi def link belDecl Structure
|
||||||
|
|
||||||
syn keyword belTotal total
|
syn keyword belTotal total
|
||||||
|
@ -38,7 +38,8 @@ hi def link belTotal Special
|
||||||
syn keyword belTrust trust
|
syn keyword belTrust trust
|
||||||
hi def link belTrust Underlined
|
hi def link belTrust Underlined
|
||||||
|
|
||||||
syn match belSubstConst /\.\.\|\^/
|
syn keyword belSubstConst ^
|
||||||
|
syn match belSubstConst /\.\./
|
||||||
hi def link belSubstConst Constant
|
hi def link belSubstConst Constant
|
||||||
|
|
||||||
syn keyword belIdBlock some block
|
syn keyword belIdBlock some block
|
||||||
|
@ -58,9 +59,9 @@ hi def link belSubstVar String
|
||||||
|
|
||||||
syn region belObjLam
|
syn region belObjLam
|
||||||
\ matchgroup=belObjLamP start=/\\/ matchgroup=belArrowEtc end=/\./ transparent
|
\ matchgroup=belObjLamP start=/\\/ matchgroup=belArrowEtc end=/\./ transparent
|
||||||
hi def link belObjLamP Define
|
hi def link belObjLamP Function
|
||||||
|
|
||||||
syn keyword belMetaLam fn mlam
|
syn keyword belMetaLam fn mlam fun
|
||||||
hi def link belMetaLam Define
|
hi def link belMetaLam Define
|
||||||
|
|
||||||
syn keyword belCase case of impossible
|
syn keyword belCase case of impossible
|
||||||
|
@ -72,14 +73,17 @@ hi def link belLet Keyword
|
||||||
syn match belSubBlock /\.\k\+\>/
|
syn match belSubBlock /\.\k\+\>/
|
||||||
hi def link belSubBlock Label
|
hi def link belSubBlock Label
|
||||||
|
|
||||||
syn keyword belBoolType Bool
|
" bools are gone
|
||||||
hi def link belBoolType Typedef
|
" but if/then/else are still keywords that don't do anything ☹
|
||||||
|
|
||||||
syn keyword belBool ttrue ffalse
|
" syn keyword belBoolType Bool
|
||||||
hi def link belBool Boolean
|
" hi def link belBoolType Typedef
|
||||||
|
|
||||||
|
" syn keyword belBool ttrue ffalse
|
||||||
|
" hi def link belBool Boolean
|
||||||
|
|
||||||
syn keyword belIf if then else
|
syn keyword belIf if then else
|
||||||
hi def link belIf Keyword
|
hi def link belIf Error
|
||||||
|
|
||||||
syn match belugaError /<-\|←/
|
syn match belugaError /<-\|←/
|
||||||
syn keyword belugaError prop
|
syn keyword belugaError prop
|
||||||
|
|
Loading…
Reference in New Issue