1 <?xml version="1.0" encoding="UTF-8"?>
2 <language id="grafite" _name="grafite" version="2.0" _section="Sources">
4 <property name="mimetypes">text/x-matita</property>
5 <property name="globs">*.ma</property>
6 <property name="block-comment-start">(*</property>
7 <property name="block-comment-end">*)</property>
11 <style id="comment" _name="Comment" map-to="def:comment"/>
12 <style id="base-n-integer" _name="Base-N Integer" map-to="def:base-n-integer"/>
13 <style id="string" _name="String" map-to="def:string"/>
14 <style id="keyword" _name="Keyword" map-to="def:keyword"/>
15 <style id="type" _name="Data Type" map-to="def:type"/>
16 <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
20 <define-regex id="cap-ident">\b[A-Z][A-Za-z0-9_']*</define-regex>
21 <define-regex id="low-ident">\b[a-z][A-Za-z0-9_']*</define-regex>
22 <define-regex id="char-esc">\\((\\|"|'|n|t|b|r)|[0-9]{3}|x[0-9a-fA-F]{2})</define-regex>
23 <context id="escape-seq" style-ref="escape">
24 <match>\%{char-esc}</match>
26 <!-- here's the main context -->
27 <context id="grafite">
29 <context id="comment" style-ref="comment">
33 <context ref="string"/>
34 <context id="comment-in-comment" style-ref="comment">
38 <context ref="string"/>
39 <context ref="comment-in-comment"/>
40 <context ref="def:in-comment:*"/>
43 <context ref="def:in-comment:*"/>
46 <context id="string" style-ref="string">
50 <context ref="escape-seq"/>
53 <context id="character-constant" style-ref="string">
54 <match>('\%{char-esc}')|('[^\\']')</match>
56 <!-- Flow control & common keywords -->
57 <context id="keywords" style-ref="keyword">
59 <keyword>theorem</keyword>
60 <keyword>definition</keyword>
61 <keyword>lemma</keyword>
62 <keyword>fact</keyword>
63 <keyword>remark</keyword>
64 <keyword>variant</keyword>
65 <keyword>axiom</keyword>
68 <keyword>ntheorem</keyword>
69 <keyword>nrecord</keyword>
70 <keyword>ndefinition</keyword>
71 <keyword>ninductive</keyword>
72 <keyword>ncoinductive</keyword>
73 <keyword>nlet</keyword>
74 <keyword>nlemma</keyword>
75 <keyword>naxiom</keyword>
78 <keyword>absurd</keyword>
79 <keyword>apply</keyword>
80 <keyword>applyP</keyword>
81 <keyword>assumption</keyword>
82 <keyword>autobatch</keyword>
83 <keyword>cases</keyword>
84 <keyword>clear</keyword>
85 <keyword>clearbody</keyword>
86 <keyword>change</keyword>
87 <keyword>compose</keyword>
88 <keyword>constructor</keyword>
89 <keyword>contradiction</keyword>
90 <keyword>cut</keyword>
91 <keyword>decompose</keyword>
92 <keyword>destruct</keyword>
93 <keyword>elim</keyword>
94 <keyword>elimType</keyword>
95 <keyword>exact</keyword>
96 <keyword>exists</keyword>
97 <keyword>fail</keyword>
98 <keyword>fold</keyword>
99 <keyword>fourier</keyword>
100 <keyword>fwd</keyword>
101 <keyword>generalize</keyword>
102 <keyword>id</keyword>
103 <keyword>intro</keyword>
104 <keyword>intros</keyword>
105 <keyword>inversion</keyword>
106 <keyword>lapply</keyword>
107 <keyword>linear</keyword>
108 <keyword>left</keyword>
109 <keyword>letin</keyword>
110 <keyword>normalize</keyword>
111 <keyword>reflexivity</keyword>
112 <keyword>replace</keyword>
113 <keyword>rewrite</keyword>
114 <keyword>ring</keyword>
115 <keyword>right</keyword>
116 <keyword>symmetry</keyword>
117 <keyword>simplify</keyword>
118 <keyword>split</keyword>
119 <keyword>to</keyword>
120 <keyword>transitivity</keyword>
121 <keyword>unfold</keyword>
122 <keyword>whd</keyword>
123 <keyword>assume</keyword>
124 <keyword>suppose</keyword>
125 <keyword>by</keyword>
126 <keyword>is</keyword>
127 <keyword>or</keyword>
128 <keyword>equivalent</keyword>
129 <keyword>equivalently</keyword>
130 <keyword>we</keyword>
131 <keyword>prove</keyword>
132 <keyword>proved</keyword>
133 <keyword>need</keyword>
134 <keyword>proceed</keyword>
135 <keyword>induction</keyword>
136 <keyword>inductive</keyword>
137 <keyword>case</keyword>
138 <keyword>base</keyword>
139 <keyword>let</keyword>
140 <keyword>such</keyword>
141 <keyword>that</keyword>
142 <keyword>by</keyword>
143 <keyword>have</keyword>
144 <keyword>and</keyword>
145 <keyword>the</keyword>
146 <keyword>thesis</keyword>
147 <keyword>becomes</keyword>
148 <keyword>hypothesis</keyword>
149 <keyword>know</keyword>
150 <keyword>case</keyword>
151 <keyword>obtain</keyword>
152 <keyword>conclude</keyword>
153 <keyword>done</keyword>
154 <keyword>rule</keyword>
157 <keyword>napply</keyword>
158 <keyword>ncases</keyword>
159 <keyword>nletin</keyword>
160 <keyword>nauto</keyword>
161 <keyword>nelim</keyword>
162 <keyword>nwhd</keyword>
163 <keyword>nnormalize</keyword>
164 <keyword>nassumption</keyword>
165 <keyword>ngeneralize</keyword>
166 <keyword>nchange</keyword>
167 <keyword>nrewrite</keyword>
168 <keyword>ncut</keyword>
169 <keyword>nlapply</keyword>
170 <keyword>ndestruct</keyword>
173 <keyword>alias</keyword>
174 <keyword>and</keyword>
175 <keyword>as</keyword>
176 <keyword>coercion</keyword>
177 <keyword>prefer</keyword>
178 <keyword>nocomposites</keyword>
179 <keyword>coinductive</keyword>
180 <keyword>corec</keyword>
181 <keyword>default</keyword>
182 <keyword>for</keyword>
183 <keyword>include</keyword>
184 <keyword>include'</keyword>
185 <keyword>inductive</keyword>
186 <keyword>inverter</keyword>
187 <keyword>in</keyword>
188 <keyword>interpretation</keyword>
189 <keyword>let</keyword>
190 <keyword>match</keyword>
191 <keyword>names</keyword>
192 <keyword>notation</keyword>
193 <keyword>on</keyword>
194 <keyword>qed</keyword>
195 <keyword>rec</keyword>
196 <keyword>record</keyword>
197 <keyword>return</keyword>
198 <keyword>source</keyword>
199 <keyword>to</keyword>
200 <keyword>using</keyword>
201 <keyword>with</keyword>
205 <keyword>unification</keyword>
206 <keyword>hint</keyword>
207 <keyword>ncoercion</keyword>
208 <keyword>ninverter</keyword>
209 <keyword>nqed</keyword>
212 <keyword>inline</keyword>
213 <keyword>procedural</keyword>
214 <keyword>check</keyword>
215 <keyword>eval</keyword>
216 <keyword>hint</keyword>
217 <keyword>set</keyword>
218 <keyword>auto</keyword>
219 <keyword>nodefaults</keyword>
220 <keyword>coercions</keyword>
221 <keyword>comments</keyword>
222 <keyword>debug</keyword>
223 <keyword>cr</keyword>
226 <keyword>ncheck</keyword>
229 <keyword>try</keyword>
230 <keyword>solve</keyword>
231 <keyword>do</keyword>
232 <keyword>repeat</keyword>
233 <keyword>first</keyword>
234 <keyword>focus</keyword>
235 <keyword>unfocus</keyword>
236 <keyword>progress</keyword>
237 <keyword>skip</keyword>
239 <context id="types" style-ref="type">
241 <keyword>Set</keyword>
242 <keyword>Prop</keyword>
243 <keyword>Type</keyword>
244 <keyword>CProp</keyword>
247 <keyword>Prop</keyword>
248 <keyword>Type[0]</keyword>
249 <keyword>CProp[0]</keyword>
250 <keyword>Type[1]</keyword>
251 <keyword>CProp[1]</keyword>
252 <keyword>Type[2]</keyword>
253 <keyword>CProp[2]</keyword>
260 <pattern-item _name = "Command [" style = "Keyword">
263 <pattern-item _name = "Command |" style = "Keyword">
266 <pattern-item _name = "Command ]" style = "Keyword">
269 <pattern-item _name = "Command {" style = "Keyword">
272 <pattern-item _name = "Command }" style = "Keyword">
275 <pattern-item _name = "Notation ast mark" style = "Keyword">
278 <pattern-item _name = "Notation meta mark" style = "Keyword">
283 <keyword-list _name = "Whelp Macro" style = "Others 3"
284 case-sensitive="TRUE"
285 beginning-regex="whelp *"
286 match-empty-string-at-beginning="FALSE"
287 match-empty-string-at-end="FALSE" >
288 <keyword>elim</keyword>
289 <keyword>hint</keyword>
290 <keyword>instance</keyword>
291 <keyword>locate</keyword>
292 <keyword>match</keyword>
295 <keyword-list _name = "TeX Macro" style = "Preprocessor"
296 case-sensitive="TRUE"
298 match-empty-string-at-beginning="FALSE"
299 match-empty-string-at-end="FALSE" >
300 <keyword>def</keyword>
301 <keyword>forall</keyword>
302 <keyword>lambda</keyword>
303 <keyword>to</keyword>
304 <keyword>exists</keyword>
305 <keyword>Rightarrow</keyword>
306 <keyword>Assign</keyword>
307 <keyword>land</keyword>
308 <keyword>lor</keyword>
309 <keyword>lnot</keyword>
310 <keyword>liff</keyword>
311 <keyword>subst</keyword>
312 <keyword>vdash</keyword>
313 <keyword>iforall</keyword>
314 <keyword>iexists</keyword>