if exists('b:current_syntax')
  finish
endif
let b:current_syntax = 'maude'

setlocal iskeyword=48-57,a-z,A-Z,!,$,&,',*,+,_,/,=,@,-,~,#,^

syn match belArrowEtc /->\|=>\|→\|←\|⇒\||-#\?\|⊢\|\<=\>\|:/
hi def link belArrowEtc Function

syn match belBrack /[()[\]{}.;,]\|\<\/\>\||-\@!/
hi def link belBrack Delimiter

syn match belComment /%\s.*$/
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
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 fun stratified proof schema rec and
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 belIdSubst /\.\./
hi def link belIdSubst Constant

syn keyword belIdBlock some block
hi def link belIdBlock Structure

syn match belVarVar /#\l\k*/
hi def link belVarVar Constant

syn match belSubstVar /#\u\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 fn mlam
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