2 " Language: B (A Formal Method with refinement and mathematical proof)
3 " Maintainer: Mathieu Clabaut <mathieu.clabaut@gmail.com>
4 " Contributor: Csaba Hoch
5 " LastChange: 8 Dec 2007
8 " For version 5.x: Clear all syntax items
9 " For version 6.x: Quit when a syntax file was already loaded
12 elseif exists("b:current_syntax")
17 " A bunch of useful B keywords
18 syn keyword bStatement MACHINE MODEL 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 XLS THEOREMS LOCAL_OPERATIONS
19 syn keyword bLabel CASE IN EITHER OR CHOICE DO OF
20 syn keyword bConditional IF ELSE SELECT ELSIF THEN WHEN
21 syn keyword bRepeat WHILE FOR
22 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
23 syn keyword bKeywords LET VAR BE IN BEGIN END POW POW1 FIN FIN1 PRE SIGMA STRING UNION IS ANY WHERE
25 syn keyword bBoolean TRUE FALSE bfalse btrue
26 syn keyword bConstant PI MAXINT MININT User_Pass PatchProver PatchProverH0 PatchProverB0 FLAT ARI DED SUB RES
27 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
29 syn keyword bLogic or not
30 syn match bLogic "\(!\|#\|%\|&\|+->>\|+->\|-->>\|->>\|-->\|->\|/:\|/<:\|/<<:\|/=\|/\\\|/|\\\|::\|:\|;:\|<+\|<->\|<--\|<-\|<:\|<<:\|<<|\|<=>\|<|\|==\|=>\|>+>>\|>->\|>+>\|||\||->\)"
31 syn match bNothing /:=/
33 syn keyword cTodo contained TODO FIXME XXX
35 " String and Character constants
36 " Highlight special characters (those which have a backslash) differently
37 syn match bSpecial contained "\\[0-7][0-7][0-7]\=\|\\."
38 syn region bString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=bSpecial
39 syn match bCharacter "'[^\\]'"
40 syn match bSpecialCharacter "'\\.'"
41 syn match bSpecialCharacter "'\\[0-7][0-7]'"
42 syn match bSpecialCharacter "'\\[0-7][0-7][0-7]'"
44 "catch errors caused by wrong parenthesis
45 syn region bParen transparent start='(' end=')' contains=ALLBUT,bParenError,bIncluded,bSpecial,bTodo,bUserLabel,bBitField
46 syn match bParenError ")"
47 syn match bInParen contained "[{}]"
49 "integer number, or floating point number without a dot and with "f".
51 syn match bNumber "\<[0-9]\+\>"
52 "syn match bIdentifier "\<[a-z_][a-z0-9_]*\>"
55 syn region bComment start="/\*" end="\*/" contains=bTodo
56 syn match bComment "//.*" contains=bTodo
57 syntax match bCommentError "\*/"
59 syn keyword bType INT INTEGER BOOL NAT NATURAL NAT1 NATURAL1
61 syn region bPreCondit start="^\s*#\s*\(if\>\|ifdef\>\|ifndef\>\|elif\>\|else\>\|endif\>\)" skip="\\$" end="$" contains=bComment,bString,bCharacter,bNumber,bCommentError
62 syn region bIncluded contained start=+"+ skip=+\\\\\|\\"+ end=+"+
63 syn match bIncluded contained "<[^>]*>"
64 syn match bInclude "^\s*#\s*include\>\s*["<]" contains=bIncluded
66 syn region bDefine start="^\s*#\s*\(define\>\|undef\>\)" skip="\\$" end="$" contains=ALLBUT,bPreCondit,bIncluded,bInclude,bDefine,bInParen
67 syn region bPreProc start="^\s*#\s*\(pragma\>\|line\>\|warning\>\|warn\>\|error\>\)" skip="\\$" end="$" contains=ALLBUT,bPreCondit,bIncluded,bInclude,bDefine,bInParen
69 syn sync ccomment bComment minlines=10
71 " Define the default highlighting.
72 " For version 5.7 and earlier: only when not done already
73 " For version 5.8 and later: only when an item doesn't have highlighting yet
75 if version >= 508 || !exists("did_b_syntax_inits")
77 let did_b_syntax_inits = 1
78 command -nargs=+ HiLink hi link <args>
80 command -nargs=+ HiLink hi def link <args>
83 " The default methods for highlighting. Can be overridden later
85 HiLink bUserLabel Label
86 HiLink bConditional Conditional
89 HiLink bCharacter Character
90 HiLink bSpecialCharacter bSpecial
93 HiLink bOctalError bError
94 HiLink bParenError bError
95 " HiLink bInParen bError
96 HiLink bCommentError bError
97 HiLink bBoolean Identifier
98 HiLink bConstant Identifier
99 HiLink bGuard Identifier
100 HiLink bOperator Operator
101 HiLink bKeywords Operator
102 HiLink bOps Identifier
103 HiLink bStructure Structure
104 HiLink bStorageClass StorageClass
105 HiLink bInclude Include
106 HiLink bPreProc PreProc
108 HiLink bIncluded bString
110 HiLink bStatement Statement
111 HiLink bPreCondit PreCondit
113 HiLink bCommentError bError
114 HiLink bCommentString bString
115 HiLink bComment2String bString
116 HiLink bCommentSkip bComment
117 HiLink bString String
118 HiLink bComment Comment
119 HiLink bSpecial SpecialChar
121 "hi link bIdentifier Identifier
125 let b:current_syntax = "b"