Compare commits

...

6 Commits

Author SHA1 Message Date
rhiannon morris 41766c5db6 no more bool 2022-07-15 14:56:32 +02:00
rhiannon morris 9fae64707e highlight \ and . the same 2022-07-15 14:55:39 +02:00
rhiannon morris c3ec8631ae fix ^ in idents 2022-07-15 14:55:23 +02:00
rhiannon morris 0c1cb6f77a fun is an expression not a decl 2022-07-15 14:55:12 +02:00
rhiannon morris f58e67db1c fix comments 2022-07-15 14:54:57 +02:00
rhiannon morris 6ae3479480 recognise #[…] and $[…] 2022-07-15 14:54:53 +02:00
1 changed files with 15 additions and 11 deletions

View File

@ -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