1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
" Vim syntax file
" Language: B (A Formal Method with refinement and mathematical proof)
" Maintainer: Mathieu Clabaut <mathieu.clabaut@free.fr>
" LastChange: 25 Apr 2001
" For version 5.x: Clear all syntax items
" For version 6.x: Quit when a syntax file was already loaded
if version < 600
syntax clear
elseif exists("b:current_syntax")
finish
endif
" A bunch of useful B keywords
syn keyword bStatement MACHINE SEES OPERATIONS INCLUDES DEFINITIONS CONSTRAINTS CONSTANTS VARIABLES CONCRETE_CONSTANTS CONCRETE_VARIABLES ABSTRACT_CONSTANTS ABSTRACT_VARIABLES HIDDEN_CONSTANTS HIDDEN_VARIABLES ASSERT ASSERTIONS EXTENDS IMPLEMENTATION REFINEMENT IMPORTS USES INITIALISATION INVARIANT PROMOTES PROPERTIES REFINES SETS VALUES VARIANT VISIBLE_CONSTANTS VISIBLE_VARIABLES THEORY
syn keyword bLabel CASE IN EITHER OR CHOICE DO OF
syn keyword bConditional IF ELSE SELECT ELSIF THEN WHEN
syn keyword bRepeat WHILE FOR
syn keyword bOps bool card conc closure closure1 dom first fnc front not or id inter iseq iseq1 iterate last max min mod perm pred prj1 prj2 ran rel rev seq seq1 size skip succ tail union
syn keyword bKeywords LET VAR BE IN BEGIN END POW POW1 FIN FIN1 PRE SIGMA STRING UNION IS ANY WHERE
syn match bKeywords "||"
syn keyword bBoolean TRUE FALSE bfalse btrue
syn keyword bConstant PI MAXINT MININT User_Pass PatchProver PatchProverH0 PatchProverB0 FLAT ARI DED SUB RES
syn keyword bGuard binhyp band bnot bguard bsearch bflat bfresh bguardi bget bgethyp barith bgetresult bresult bgoal bmatch bmodr bnewv bnum btest bpattern bprintf bwritef bsubfrm bvrb blvar bcall bappend bclose
syn keyword bLogic or not
syn match bLogic "\&\|=>\|<=>"
syn keyword cTodo contained TODO FIXME XXX
" String and Character constants
" Highlight special characters (those which have a backslash) differently
syn match bSpecial contained "\\[0-7][0-7][0-7]\=\|\\."
syn region bString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=bSpecial
syn match bCharacter "'[^\\]'"
syn match bSpecialCharacter "'\\.'"
syn match bSpecialCharacter "'\\[0-7][0-7]'"
syn match bSpecialCharacter "'\\[0-7][0-7][0-7]'"
"catch errors caused by wrong parenthesis
syn region bParen transparent start='(' end=')' contains=ALLBUT,bParenError,bIncluded,bSpecial,bTodo,bUserLabel,bBitField
syn match bParenError ")"
syn match bInParen contained "[{}]"
"integer number, or floating point number without a dot and with "f".
syn case ignore
syn match bNumber "\<[0-9]\+\>"
"syn match bIdentifier "\<[a-z_][a-z0-9_]*\>"
syn case match
if exists("b_comment_strings")
" A comment can contain bString, bCharacter and bNumber.
" But a "*/" inside a bString in a bComment DOES end the comment! So we
" need to use a special type of bString: bCommentString, which also ends on
" "*/", and sees a "*" at the start of the line as comment again.
" Unfortunately this doesn't very well work for // type of comments :-(
syntax match bCommentSkip contained "^\s*\*\($\|\s\+\)"
syntax region bCommentString contained start=+"+ skip=+\\\\\|\\"+ end=+"+ end=+\*/+me=s-1 contains=bSpecial,bCommentSkip
syntax region bComment2String contained start=+"+ skip=+\\\\\|\\"+ end=+"+ end="$" contains=bSpecial
syntax region bComment start="/\*" end="\*/" contains=bTodo,bCommentString,bCharacter,bNumber,bFloat
syntax region bComment start="/\?\*" end="\*\?/" contains=bTodo,bCommentString,bCharacter,bNumber,bFloat
syntax match bComment "//.*" contains=bTodo,bComment2String,bCharacter,bNumber
else
syn region bComment start="/\*" end="\*/" contains=bTodo
syn region bComment start="/\?\*" end="\*\?/" contains=bTodo
syn match bComment "//.*" contains=bTodo
endif
syntax match bCommentError "\*/"
syn keyword bType INT INTEGER BOOL NAT NATURAL NAT1 NATURAL1
syn region bPreCondit start="^\s*#\s*\(if\>\|ifdef\>\|ifndef\>\|elif\>\|else\>\|endif\>\)" skip="\\$" end="$" contains=bComment,bString,bCharacter,bNumber,bCommentError
syn region bIncluded contained start=+"+ skip=+\\\\\|\\"+ end=+"+
syn match bIncluded contained "<[^>]*>"
syn match bInclude "^\s*#\s*include\>\s*["<]" contains=bIncluded
syn region bDefine start="^\s*#\s*\(define\>\|undef\>\)" skip="\\$" end="$" contains=ALLBUT,bPreCondit,bIncluded,bInclude,bDefine,bInParen
syn region bPreProc start="^\s*#\s*\(pragma\>\|line\>\|warning\>\|warn\>\|error\>\)" skip="\\$" end="$" contains=ALLBUT,bPreCondit,bIncluded,bInclude,bDefine,bInParen
syn sync ccomment bComment minlines=10
" Define the default highlighting.
" For version 5.7 and earlier: only when not done already
" For version 5.8 and later: only when an item doesn't have highlighting yet
if version >= 508 || !exists("did_b_syntax_inits")
if version < 508
let did_b_syntax_inits = 1
command -nargs=+ HiLink hi link <args>
else
command -nargs=+ HiLink hi def link <args>
endif
" The default methods for highlighting. Can be overridden later
HiLink bLabel Label
HiLink bUserLabel Label
HiLink bConditional Conditional
HiLink bRepeat Repeat
HiLink bLogic Special
HiLink bCharacter Character
HiLink bSpecialCharacter bSpecial
HiLink bNumber Number
HiLink bFloat Float
HiLink bOctalError bError
HiLink bParenError bError
" HiLink bInParen bError
HiLink bCommentError bError
HiLink bBoolean Identifier
HiLink bConstant Identifier
HiLink bGuard Identifier
HiLink bOperator Operator
HiLink bKeywords Operator
HiLink bOps Identifier
HiLink bStructure Structure
HiLink bStorageClass StorageClass
HiLink bInclude Include
HiLink bPreProc PreProc
HiLink bDefine Macro
HiLink bIncluded bString
HiLink bError Error
HiLink bStatement Statement
HiLink bPreCondit PreCondit
HiLink bType Type
HiLink bCommentError bError
HiLink bCommentString bString
HiLink bComment2String bString
HiLink bCommentSkip bComment
HiLink bString String
HiLink bComment Comment
HiLink bSpecial SpecialChar
HiLink bTodo Todo
"hi link bIdentifier Identifier
delcommand HiLink
endif
let current_syntax = "b"
" vim: ts=8
|
