" Vim syntax file
" Language:     Fellowship
" Filenames:    *.fsp
" Maintainers:  Florent Kirchner
" URL: http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/doc/fsp.vim
" Last Change:  2006 June 13 - Added open.

" Clear all syntax items
syntax clear

" Fellowship is case sensitive
syntax case match

"Errors
"syntax match 	fspError "cut \w"
syntax keyword 	fspError error

" Comments
syntax region	fspComment start="(\*" end="\*)\|$" contains=fspComment,fspTodo
syntax keyword	fspTodo contained TODO forge

" Logics
syntax keyword 	fspLogic true false
syntax match 	fspLogic "\~" 
syntax match 	fspLogic "\\/" 
syntax match 	fspLogic "/\\" 
syntax match 	fspLogic "-\(>\)\="
syntax region	fspLogic matchgroup=fspLogic start="exists\|forall" end=":" contains=fspLabel nextgroup=fspQuantType skipwhite
syntax match 	fspQuantType "\w\+" contained skipwhite

" Instructions
syntax keyword 	fspType bool type

syntax region	fspKeyword matchgroup=fspKeyword start="open" end="\." contains=fspLabel

syntax match 	fspLabel "\h\w*" contained
syntax region 	fspKeyword matchgroup=fspKeyword start="declare\|theorem" end=":" contains=fspLabel
syntax keyword 	fspKeyword qed

syntax keyword 	fspKeyword lj lk minimal full
syntax match 	fspKeyword "discard \(all\|theorem\)"
syntax keyword 	fspKeyword next prev
syntax keyword 	fspKeyword quit
syntax match 	fspKeyword "\."

" Tactics
syntax keyword 	fspTactic axiom cut apply
"syntax match 	fspTactic "cut" nextgroup=fspCutProp skipwhite
"syntax match 	fspCutProp "(\(\w\|\[\|\]\)*)" contained nextgroup=fspLabel skipwhite

"syntax match 	fspTactic "elim \(in \w \w\)\="
syntax keyword 	fspTactic focus contraction weaken idtac elim in
syntax match 	fspTactic ";\|\[\|\]\||"

" Define the default highlighting.
hi link fspComment 	Comment
hi link fspTodo		Todo
hi link fspKeyword 	Keyword
hi link fspLogic 	Include
hi link fspType		Constant
hi link fspLabel	Identifier
hi link fspTactic	Type
hi link fspError	Error

hi link fspQuantType	Identifier
hi link fspCutProp 	Include

let b:current_syntax = "fsp"