rhi
/
beluga.vim
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Compare commits

base: rhi:3229be14f8f3d356f9543e52bf985e7f206b153a
Branches Tags
rhi:main
...
compare: rhi:41766c5db6686df29b3c4cf8b1b7e9058d92c75f
Branches Tags
rhi:main

6 Commits
3229be14f8 ... 41766c5db6

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
Show Stats Expand all files Collapse all files

26
syntax/beluga.vim
View File

@ -10,10 +10,10 @@ setlocal commentstring=%%s
syn match belArrowEtc /->\|=>\|→\|⇒\||-#\?\|⊢\|\<=\>\|:/
hi def link belArrowEtc Function
syn match belDelim /[()[\]{}.;,]\|\<\/\>\||-\@!\|<\|-\@<!>/
syn match belDelim /[()\]{}.;,]\|[#$]\?\[\|\<\/\>\||-\@!\|<\|-\@<!>/
hi def link belDelim Delimiter
syn match belComment /%\+\s.*$/
syn match belComment /%.*$/
hi def link belComment Comment
syn region belBlockComment start='%{' end='}%' contains=belBlockComment
@ -29,7 +29,7 @@ syn match belPragma /\%(%\|\<--\)\%(coverage\|warncoverage\|nostrengthen\|infix\
hi def link belPragma Special
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
syn keyword belTotal total
@ -38,7 +38,8 @@ hi def link belTotal Special
syn keyword belTrust trust
hi def link belTrust Underlined
syn match belSubstConst /\.\.\|\^/
syn keyword belSubstConst ^
syn match belSubstConst /\.\./
hi def link belSubstConst Constant
syn keyword belIdBlock some block
@ -58,9 +59,9 @@ hi def link belSubstVar String
syn region belObjLam
\ 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
syn keyword belCase case of impossible
@ -72,14 +73,17 @@ hi def link belLet Keyword
syn match belSubBlock /\.\k\+\>/
hi def link belSubBlock Label
syn keyword belBoolType Bool
hi def link belBoolType Typedef
" bools are gone
" but if/then/else are still keywords that don't do anything ☹
syn keyword belBool ttrue ffalse
hi def link belBool Boolean
" 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
hi def link belIf Error
syn match belugaError /<-\|←/
syn keyword belugaError prop