forked from tamarin-prover/tamarin-prover
-
Notifications
You must be signed in to change notification settings - Fork 0
/
spthy.vim
212 lines (189 loc) · 8.19 KB
/
spthy.vim
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
" Vim syntax file
" Language: DH-proto-proof Security Protocol Theory Files
" Maintainer: Nick Moore <[email protected]>
" Last Change: 2018 04 10
" based on Claudio Fleiner's <[email protected]> spthy syntax highlighting
" file.
" Quit when a syntax file was already loaded
if !exists("main_syntax")
if version < 600
syntax clear
elseif exists("b:current_syntax")
finish
endif
" we define it here so that included files can test for it
let main_syntax='spthy'
syn region spthyFold start="{" end="}" transparent fold
endif
" don't use standard HiLink, it will not work with included syntax files
if version < 508
command! -nargs=+ SpthyHiLink hi link <args>
else
command! -nargs=+ SpthyHiLink hi def link <args>
endif
" some characters that cannot be in a spthy program (outside a string)
" syn match spthyError "[\\@`]"
" syn match spthyError "<<<\|\.\.\|=>\|<>\|||=\|&&=\|[^-]->\|\*\/"
" syn match spthyOK "\.\.\."
syn match spthyLAtom ":>"
syn match spthyLAtom "--|"
syn match spthyLAtom "<:"
syn match spthyLAtom ">+>"
syn match spthyLAtom ">->"
syn match spthyLAtom "="
syn match spthyLAtom "@"
syn match spthyLAtom "<"
syn match spthyLAtom ">"
syn keyword spthyConstr aenc sdec senc sdec sign verify hashing signing multiset
syn match spthyConstr "\<h("he=e-1
syn match spthyConstr "\<sk("he=e-1
syn match spthyConstr "\<pk("he=e-1
syn match spthyConstr "\<fr("he=e-1
syn match spthyConstr "\<pb("he=e-1
syn match spthyConstr "\<lts("he=e-1
syn match spthyConstr "*"
syn match spthyConstr "\^"
syn match spthyConstr "\<diffie-hellman"
syn match spthyConstr "\<symmetric-encryption"
syn match spthyConstr "\<asymmetric-encryption"
syn keyword spthyDecl axiom restriction equations functions builtins protocol property in let theory begin end subsection section text
syn match spthyDecl "\<lemma\>"
syn match spthyDecl "\<exists-trace"
syn match spthyDecl "\<all-traces"
syn match spthyDecl "\<enable"
syn match spthyDecl "\<rule"
syn match spthyDecl "\<assertions"
syn match spthyDecl "\<modulo"
syn match spthyDecl "\<default_rules"
syn match spthyDecl "\<anb-proto"
syn match spthyDecl ":"
syn match spthyDecl "{\*"
syn match spthyDecl "\*}"
syn match spthyDecl "\""
syn match spthyDecl "[a-zA-Z\-_]\@<!\d\+\."
syn match spthyTransfer "->"
syn match spthyTransfer "<-"
syn match spthyDecl "-->"
syn match spthyDecl "--\["
syn match spthyDecl "\]->"
syn region spthyLiteral start="'" end="'"
syn keyword spthyAnnot contained use_induction sources reuse hide_lemma left right
syn region spthyAnnotLemma matchgroup=spthyDecl start="\<lemma\>" skip="(\s\+\w\+\s*\[|\])" end=":" matchgroup=NONE contains=spthyAnnot
syn match spthyLogicOp "==>"
syn match spthyLogicOp "<=>"
syn keyword spthyLogicOp F T All Ex
syn match spthyLogicOp "|"
syn match spthyLogicOp "&"
syn match spthyLogicOp "\."
" The following cluster contains all spthy groups except the contained ones
syn cluster spthyTop add=spthyLAtom,spthyDecl
" Comments
syn keyword spthyTodo contained TODO FIXME XXX
syn region spthyComment start="/\*" end="\*/" contains=spthyTodo
syn match spthyLineComment "//.*" contains=spthyTodo
syn cluster spthyTop add=spthyComment,spthyLineComment
" Strings and constants
" syn match spthySpecialError contained "\\."
" syn match spthySpecialCharError contained "[^']"
" syn match spthySpecialChar contained "\\\([4-9]\d\|[0-3]\d\d\|[\"\\'ntbrf]\|u\+\x\{4\}\)"
" syn region spthyString start=+"+ end=+"+ end=+$+ contains=spthySpecialChar,spthySpecialError,@Spell
" " next line disabled, it can cause a crash for a long line
" "syn match spthyStringError +"\([^"\\]\|\\.\)*$+
" syn match spthyCharacter "'[^']*'" contains=spthySpecialChar,spthySpecialCharError
" syn match spthyCharacter "'\\''" contains=spthySpecialChar
" syn match spthyCharacter "'[^\\]'"
" syn match spthyNumber "\<\(0[0-7]*\|0[xX]\x\+\|\d\+\)[lL]\=\>"
" syn match spthyNumber "\(\<\d\+\.\d*\|\.\d\+\)\([eE][-+]\=\d\+\)\=[fFdD]\="
" syn match spthyNumber "\<\d\+[eE][-+]\=\d\+[fFdD]\=\>"
" syn match spthyNumber "\<\d\+\([eE][-+]\=\d\+\)\=[fFdD]\>"
"
" " unicode characters
" syn match spthySpecial "\\u\+\d\{4\}"
"
" syn cluster spthyTop add=spthyString,spthyCharacter,spthyNumber,spthySpecial,spthyStringError
" catch errors caused by wrong parenthesis
" syn region spthyParenT transparent matchgroup=spthyParen start="(" end=")" contains=@spthyTop,spthyParenT1
" syn region spthyParenT1 transparent matchgroup=spthyParen1 start="(" end=")" contains=@spthyTop,spthyParenT2 contained
" syn region spthyParenT2 transparent matchgroup=spthyParen2 start="(" end=")" contains=@spthyTop,spthyParenT contained
" syn match spthyParenError ")"
" " catch errors caused by wrong square parenthesis
" syn region spthyParenT transparent matchgroup=spthyParen start="\[" end="\]" contains=@spthyTop,spthyParenT1
" syn region spthyParenT1 transparent matchgroup=spthyParen1 start="\[" end="\]" contains=@spthyTop,spthyParenT2 contained
" syn region spthyParenT2 transparent matchgroup=spthyParen2 start="\[" end="\]" contains=@spthyTop,spthyParenT contained
" syn match spthyParenError "\]"
"
" SpthyHiLink spthyParenError spthyError
if !exists("spthy_minlines")
let spthy_minlines = 10
endif
exec "syn sync ccomment spthyComment minlines=" . spthy_minlines
" The default highlighting.
if version >= 508 || !exists("did_spthy_syn_inits")
if version < 508
let did_spthy_syn_inits = 1
endif
SpthyHiLink spthyLAtom Operator
SpthyHiLink spthyComment Comment
SpthyHiLink spthyDocComment Comment
SpthyHiLink spthyLineComment Comment
SpthyHiLink spthyError Error
SpthyHiLink spthyDecl Typedef
SpthyHiLink spthyTransfer Typedef
SpthyHiLink spthyConstr Function
SpthyHiLink spthyAnnot Label
SpthyHiLink spthyLiteral String
SpthyHiLink spthyTODO Todo
SpthyHiLink spthyLogicOp Boolean
" SpthyHiLink spthyVarArg Function
" SpthyHiLink spthyBraces Function
" SpthyHiLink spthyBranch Conditional
" SpthyHiLink spthyUserLabelRef spthyUserLabel
" SpthyHiLink spthyLabel Label
" SpthyHiLink spthyUserLabel Label
" SpthyHiLink spthyConditional Conditional
" SpthyHiLink spthyRepeat Repeat
" SpthyHiLink spthyExceptions Exception
" SpthyHiLink spthyAssert Statement
" SpthyHiLink spthyStorageClass StorageClass
" SpthyHiLink spthyMethodDecl spthyStorageClass
" SpthyHiLink spthyClassDecl spthyStorageClass
" SpthyHiLink spthyScopeDecl spthyStorageClass
" SpthyHiLink spthyBoolean Boolean
" SpthyHiLink spthySpecial Special
" SpthyHiLink spthySpecialError Error
" SpthyHiLink spthySpecialCharError Error
" SpthyHiLink spthyString String
" SpthyHiLink spthyCharacter Character
" SpthyHiLink spthySpecialChar SpecialChar
" SpthyHiLink spthyNumber Number
" SpthyHiLink spthyStringError Error
" SpthyHiLink spthyStatement Statement
" SpthyHiLink spthyOperator Operator
" SpthyHiLink spthyComment Comment
" SpthyHiLink spthyDocComment Comment
" SpthyHiLink spthyLineComment Comment
" SpthyHiLink spthyConstant Constant
" SpthyHiLink spthyTypedef Typedef
" SpthyHiLink spthyTodo Todo
" SpthyHiLink spthyAnnotation PreProc
"
" SpthyHiLink spthyCommentTitle SpecialComment
" SpthyHiLink spthyDocTags Special
" SpthyHiLink spthyDocParam Function
" SpthyHiLink spthyDocSeeTagParam Function
" SpthyHiLink spthyCommentStar spthyComment
"
" SpthyHiLink spthyType Type
" SpthyHiLink spthyExternal Include
"
" SpthyHiLink htmlComment Special
" SpthyHiLink htmlCommentPart Special
" SpthyHiLink spthySpaceError Error
endif
delcommand SpthyHiLink
let b:current_syntax = "spthy"
if main_syntax == 'spthy'
unlet main_syntax
endif
let b:spell_options="contained"
" vim: ts=8