]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/matita.lang
update in static_2
[helm.git] / matita / matita / matita.lang
1 <?xml version="1.0" encoding="UTF-8"?>
2 <language id="grafite" _name="grafite" version="2.0" _section="Sources">
3   <metadata>
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>
8   </metadata>
9
10   <styles>
11     <style id="comment" _name="Comment" map-to="def:comment"/>
12     <style id="string" _name="String" map-to="def:string"/>
13     <style id="escape" _name="Escape" 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="latex" _name="LaTeX Escaped" map-to="def:special-char"/>
17     <style id="macros" _name="Macros" map-to="def:keyword"/>
18     <style id="tinycals" _name="Tinycals" map-to="def:keyword"/>
19     <style id="quantifiers" _name="Quantifiers" map-to="def:type"/>
20   </styles>
21
22   <definitions>
23     <define-regex id="char-esc">\\"|[0-9a-zA-Z]</define-regex>
24     <context id="escape-seq" style-ref="escape">
25       <match>\%{char-esc}</match>
26     </context>
27     <!-- here's the main context -->
28     <context id="grafite">
29       <include>
30         <context id="comment" style-ref="comment">
31           <start>\(\*</start>
32           <end>\*\)</end>
33           <include>
34             <context ref="string"/>
35             <context id="comment-in-comment" style-ref="comment">
36               <start>\(\*</start>
37               <end>\*\)</end>
38               <include>
39                 <context ref="string"/>
40                 <context ref="comment-in-comment"/>
41                 <context ref="def:in-comment:*"/>
42               </include>
43             </context>
44             <context ref="def:in-comment:*"/>
45           </include>
46         </context>
47         <context id="string" style-ref="string">
48           <start>"</start>
49           <end>"</end>
50           <include>
51             <context ref="escape-seq"/>
52           </include>
53         </context>
54         <context id="character-constant" style-ref="string">
55           <match>('\%{char-esc}')|('[^\\']')</match>
56         </context>
57         <context id="latex" style-ref="latex">
58          <prefix>\\</prefix>
59          <keyword>def</keyword>
60          <keyword>forall</keyword>
61          <keyword>lambda</keyword>
62          <keyword>to</keyword>
63          <keyword>exists</keyword>
64          <keyword>Rightarrow</keyword>
65          <keyword>Assign</keyword>
66          <keyword>land</keyword>
67          <keyword>lor</keyword>
68          <keyword>lnot</keyword>
69          <keyword>liff</keyword>
70          <keyword>subst</keyword>
71          <keyword>vdash</keyword>
72          <keyword>iforall</keyword>
73          <keyword>iexists</keyword>
74         </context>
75         <!-- Flow control & common keywords -->
76         <context id="keywords" style-ref="keyword">
77
78          <!-- source -->
79          <keyword>implied</keyword>
80
81          <!-- objects -->
82          <keyword>theorem</keyword>
83          <keyword>record</keyword>
84          <keyword>definition</keyword>
85          <keyword>inductive</keyword>
86          <keyword>coinductive</keyword>
87          <keyword>fact</keyword>
88          <keyword>lemma</keyword>
89          <keyword>remark</keyword>
90          <keyword>axiom</keyword>
91
92          <!-- tactics -->
93          <keyword>apply</keyword>
94          <keyword>applyS</keyword>
95          <keyword>cases</keyword>
96          <keyword>letin</keyword>
97          <keyword>auto</keyword>
98          <keyword>elim</keyword>
99          <keyword>whd</keyword>
100          <keyword>normalize</keyword>
101          <keyword>assumption</keyword>
102          <keyword>generalize</keyword>
103          <keyword>change</keyword>
104          <keyword>rewrite</keyword>
105          <keyword>cut</keyword>
106          <keyword>inversion</keyword>
107          <keyword>lapply</keyword>
108          <keyword>destruct</keyword>
109          <keyword>assume</keyword>
110          <keyword>suppose</keyword>
111          <keyword>that</keyword>
112          <keyword>is</keyword>
113          <keyword>equivalent</keyword>
114          <keyword>to</keyword>
115          <keyword>we</keyword> 
116          <keyword>need</keyword> 
117          <keyword>prove</keyword> 
118          <keyword>or</keyword> 
119          <keyword>equivalently</keyword> 
120          <keyword>by</keyword> 
121          <keyword>done</keyword> 
122          <keyword>proved</keyword> 
123          <keyword>have</keyword> 
124          <keyword>such</keyword> 
125          <keyword>the</keyword> 
126          <keyword>thesis</keyword> 
127          <keyword>becomes</keyword> 
128          <keyword>conclude</keyword> 
129          <keyword>obtain</keyword> 
130          <keyword>proceed</keyword> 
131          <keyword>induction</keyword> 
132          <keyword>case</keyword> 
133          <keyword>hypothesis</keyword> 
134          <keyword>know</keyword> 
135
136           <!-- commands -->
137           <keyword>alias</keyword>
138           <keyword>and</keyword>
139           <keyword>as</keyword>
140           <keyword>associative</keyword>
141           <keyword>coercion</keyword>
142           <keyword>prefer</keyword>
143           <keyword>nocomposites</keyword>
144           <keyword>coinductive</keyword>
145           <keyword>constraint</keyword>
146           <keyword>corec</keyword>
147           <keyword>cyclic</keyword>
148           <keyword>default</keyword>
149           <keyword>discriminator</keyword>
150           <keyword>for</keyword>
151           <keyword>id</keyword>
152           <keyword>include</keyword>
153           <keyword>include'</keyword>
154           <keyword>inductive</keyword>
155           <keyword>inverter</keyword>
156           <keyword>in</keyword>
157           <keyword>interpretation</keyword>
158           <keyword>left</keyword>
159           <keyword>let</keyword>
160           <keyword>match</keyword>
161           <keyword>names</keyword>
162           <keyword>non</keyword>
163           <keyword>notation</keyword>
164           <keyword>on</keyword>
165           <keyword>precedence</keyword>
166           <keyword>qed</keyword>
167           <keyword>defined</keyword>
168           <keyword>rec</keyword>
169           <keyword>record</keyword>
170           <keyword>return</keyword>
171           <keyword>right</keyword>
172           <keyword>source</keyword>
173           <keyword>symbol</keyword>
174           <keyword>to</keyword>
175           <keyword>universe</keyword>
176           <keyword>using</keyword>
177           <keyword>with</keyword>
178
179
180           <!-- commands -->
181           <keyword>unification</keyword>
182           <keyword>hint</keyword>
183           <keyword>coercion</keyword>
184           <keyword>inverter</keyword>
185           <keyword>qed</keyword>
186
187           <!-- macros -->
188           <keyword>check</keyword>
189           <keyword>eval</keyword>
190           <keyword>hint</keyword>
191           <keyword>set</keyword>
192           <keyword>auto</keyword>
193           <keyword>nodefaults</keyword>
194           <keyword>coercions</keyword>
195           <keyword>comments</keyword>
196           <keyword>debug</keyword>
197
198           <!-- tinycals -->
199           <keyword>try</keyword>
200           <keyword>solve</keyword>
201           <keyword>do</keyword>
202           <keyword>repeat</keyword>
203           <keyword>first</keyword>
204           <keyword>focus</keyword>
205           <keyword>unfocus</keyword>
206           <keyword>progress</keyword>
207           <keyword>skip</keyword>
208         </context>
209         <context id="types" style-ref="type">
210           <!-- sorts -->
211           <keyword>Prop</keyword>
212           <keyword>Type[0]</keyword>
213           <keyword>CProp[0]</keyword>
214           <keyword>Type[1]</keyword>
215           <keyword>CProp[1]</keyword>
216           <keyword>Type[2]</keyword>
217           <keyword>CProp[2]</keyword>
218         </context>
219         <context id="quantifiers" style-ref="quantifiers">
220           <!-- quantifiers -->
221           <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
222         </context>
223         <context id="tinycals" style-ref="tinycals">
224                 <match>\[|\||\]|\{|\}|>|//|&lt;|@|\$|#|\\\\|;|\.|:>|:|-</match>
225         </context>
226       </include>
227     </context>
228   </definitions>
229 </language>