helm/software/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="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="latex" _name="LaTeX Escaped" map-to="def:special-char"/>
  17     <style id="macros" _name="Macros" map-to="def:keyword"/>
  18     <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
  19   </styles>
  20
  21   <definitions>
  22     <define-regex id="cap-ident">\b[A-Z][A-Za-z0-9_']*</define-regex>
  23     <define-regex id="low-ident">\b[a-z][A-Za-z0-9_']*</define-regex>
  24     <define-regex id="char-esc">\\((\\|"|'|n|t|b|r)|[0-9]{3}|x[0-9a-fA-F]{2})</define-regex>
  25     <context id="escape-seq" style-ref="escape">
  26       <match>\%{char-esc}</match>
  27     </context>
  28     <!-- here's the main context -->
  29     <context id="grafite">
  30       <include>
  31         <context id="comment" style-ref="comment">
  32           <start>\(\*</start>
  33           <end>\*\)</end>
  34           <include>
  35             <context ref="string"/>
  36             <context id="comment-in-comment" style-ref="comment">
  37               <start>\(\*</start>
  38               <end>\*\)</end>
  39               <include>
  40                 <context ref="string"/>
  41                 <context ref="comment-in-comment"/>
  42                 <context ref="def:in-comment:*"/>
  43               </include>
  44             </context>
  45             <context ref="def:in-comment:*"/>
  46           </include>
  47         </context>
  48         <context id="string" style-ref="string">
  49           <start>"</start>
  50           <end>"</end>
  51           <include>
  52             <context ref="escape-seq"/>
  53           </include>
  54         </context>
  55         <context id="character-constant" style-ref="string">
  56           <match>('\%{char-esc}')|('[^\\']')</match>
  57         </context>
  58         <context id="whelp_macros" style-ref="macros">
  59          <prefix>whelp *</prefix>
  60          <keyword>elim</keyword>
  61          <keyword>hint</keyword>
  62          <keyword>instance</keyword>
  63          <keyword>locate</keyword>
  64          <keyword>match</keyword>
  65         </context>
  66         <context id="latex" style-ref="latex">
  67          <prefix>\\</prefix>
  68          <keyword>def</keyword>
  69          <keyword>forall</keyword>
  70          <keyword>lambda</keyword>
  71          <keyword>to</keyword>
  72          <keyword>exists</keyword>
  73          <keyword>Rightarrow</keyword>
  74          <keyword>Assign</keyword>
  75          <keyword>land</keyword>
  76          <keyword>lor</keyword>
  77          <keyword>lnot</keyword>
  78          <keyword>liff</keyword>
  79          <keyword>subst</keyword>
  80          <keyword>vdash</keyword>
  81          <keyword>iforall</keyword>
  82          <keyword>iexists</keyword>
  83         </context>
  84         <!-- Flow control & common keywords -->
  85         <context id="keywords" style-ref="keyword">
  86          <!-- objects -->
  87          <keyword>theorem</keyword>
  88          <keyword>definition</keyword>
  89          <keyword>lemma</keyword>
  90          <keyword>fact</keyword>
  91          <keyword>remark</keyword>
  92          <keyword>variant</keyword>
  93          <keyword>axiom</keyword>
  94
  95          <!-- nobjects -->
  96          <keyword>ntheorem</keyword>
  97          <keyword>nrecord</keyword>
  98          <keyword>ndefinition</keyword>
  99          <keyword>ninductive</keyword>
 100          <keyword>ncoinductive</keyword>
 101          <keyword>nlet</keyword>
 102          <keyword>nlemma</keyword>
 103          <keyword>naxiom</keyword>
 104
 105          <!-- tactics -->
 106          <keyword>absurd</keyword>
 107          <keyword>apply</keyword>
 108          <keyword>applyP</keyword>
 109          <keyword>assumption</keyword>
 110          <keyword>autobatch</keyword>
 111          <keyword>cases</keyword>
 112          <keyword>clear</keyword>
 113          <keyword>clearbody</keyword>
 114          <keyword>change</keyword>
 115          <keyword>compose</keyword>
 116          <keyword>constructor</keyword>
 117          <keyword>contradiction</keyword>
 118          <keyword>cut</keyword>
 119          <keyword>decompose</keyword>
 120          <keyword>destruct</keyword>
 121          <keyword>elim</keyword>
 122          <keyword>elimType</keyword>
 123          <keyword>exact</keyword>
 124          <keyword>exists</keyword>
 125          <keyword>fail</keyword>
 126          <keyword>fold</keyword>
 127          <keyword>fourier</keyword>
 128          <keyword>fwd</keyword>
 129          <keyword>generalize</keyword>
 130          <keyword>id</keyword>
 131          <keyword>intro</keyword>
 132          <keyword>intros</keyword>
 133          <keyword>inversion</keyword>
 134          <keyword>lapply</keyword>
 135          <keyword>linear</keyword>
 136          <keyword>left</keyword>
 137          <keyword>letin</keyword>
 138          <keyword>normalize</keyword>
 139          <keyword>reflexivity</keyword>
 140          <keyword>replace</keyword>
 141          <keyword>rewrite</keyword>
 142          <keyword>ring</keyword>
 143          <keyword>right</keyword>
 144          <keyword>symmetry</keyword>
 145          <keyword>simplify</keyword>
 146          <keyword>split</keyword>
 147          <keyword>to</keyword>
 148          <keyword>transitivity</keyword>
 149          <keyword>unfold</keyword>
 150          <keyword>whd</keyword>
 151          <keyword>assume</keyword>
 152          <keyword>suppose</keyword>
 153          <keyword>by</keyword>
 154          <keyword>is</keyword>
 155          <keyword>or</keyword>
 156          <keyword>equivalent</keyword>
 157          <keyword>equivalently</keyword>
 158          <keyword>we</keyword>
 159          <keyword>prove</keyword>
 160          <keyword>proved</keyword>
 161          <keyword>need</keyword>
 162          <keyword>proceed</keyword>
 163          <keyword>induction</keyword>
 164          <keyword>inductive</keyword>
 165          <keyword>case</keyword>
 166          <keyword>base</keyword>
 167          <keyword>let</keyword>
 168          <keyword>such</keyword>
 169          <keyword>that</keyword>
 170          <keyword>by</keyword>
 171          <keyword>have</keyword>
 172          <keyword>and</keyword>
 173          <keyword>the</keyword>
 174          <keyword>thesis</keyword>
 175          <keyword>becomes</keyword>
 176          <keyword>hypothesis</keyword>
 177          <keyword>know</keyword>
 178          <keyword>case</keyword>
 179          <keyword>obtain</keyword>
 180          <keyword>conclude</keyword>
 181          <keyword>done</keyword>
 182          <keyword>rule</keyword>
 183
 184          <!-- ntactics -->
 185          <keyword>napply</keyword>
 186          <keyword>ncases</keyword>
 187          <keyword>nletin</keyword>
 188          <keyword>nauto</keyword>
 189          <keyword>nelim</keyword>
 190          <keyword>nwhd</keyword>
 191          <keyword>nnormalize</keyword>
 192          <keyword>nassumption</keyword>
 193          <keyword>ngeneralize</keyword>
 194          <keyword>nchange</keyword>
 195          <keyword>nrewrite</keyword>
 196          <keyword>ncut</keyword>
 197          <keyword>nlapply</keyword>
 198          <keyword>ndestruct</keyword>
 199
 200           <!-- commands -->
 201           <keyword>alias</keyword>
 202           <keyword>and</keyword>
 203           <keyword>as</keyword>
 204           <keyword>coercion</keyword>
 205           <keyword>prefer</keyword>
 206           <keyword>nocomposites</keyword>
 207           <keyword>coinductive</keyword>
 208           <keyword>corec</keyword>
 209           <keyword>default</keyword>
 210           <keyword>for</keyword>
 211           <keyword>include</keyword>
 212           <keyword>include'</keyword>
 213           <keyword>inductive</keyword>
 214           <keyword>inverter</keyword>
 215           <keyword>in</keyword>
 216           <keyword>interpretation</keyword>
 217           <keyword>let</keyword>
 218           <keyword>match</keyword>
 219           <keyword>names</keyword>
 220           <keyword>notation</keyword>
 221           <keyword>on</keyword>
 222           <keyword>qed</keyword>
 223           <keyword>rec</keyword>
 224           <keyword>record</keyword>
 225           <keyword>return</keyword>
 226           <keyword>source</keyword>
 227           <keyword>to</keyword>
 228           <keyword>using</keyword>
 229           <keyword>with</keyword>
 230
 231
 232           <!-- ncommands -->
 233           <keyword>unification</keyword>
 234           <keyword>hint</keyword>
 235           <keyword>ncoercion</keyword>
 236           <keyword>ninverter</keyword>
 237           <keyword>nqed</keyword>
 238
 239           <!-- macros -->
 240           <keyword>inline</keyword>
 241           <keyword>procedural</keyword>
 242           <keyword>check</keyword>
 243           <keyword>eval</keyword>
 244           <keyword>hint</keyword>
 245           <keyword>set</keyword>
 246           <keyword>auto</keyword>
 247           <keyword>nodefaults</keyword>
 248           <keyword>coercions</keyword>
 249           <keyword>comments</keyword>
 250           <keyword>debug</keyword>
 251           <keyword>cr</keyword>
 252
 253           <!-- nmacros -->
 254           <keyword>ncheck</keyword>
 255
 256           <!-- tinycals -->
 257           <keyword>try</keyword>
 258           <keyword>solve</keyword>
 259           <keyword>do</keyword>
 260           <keyword>repeat</keyword>
 261           <keyword>first</keyword>
 262           <keyword>focus</keyword>
 263           <keyword>unfocus</keyword>
 264           <keyword>progress</keyword>
 265           <keyword>skip</keyword>
 266         </context>
 267         <context id="types" style-ref="type">
 268           <!-- sorts -->
 269           <keyword>Set</keyword>
 270           <keyword>Prop</keyword>
 271           <keyword>Type</keyword>
 272           <keyword>CProp</keyword>
 273
 274           <!-- nsorts -->
 275           <keyword>Prop</keyword>
 276           <keyword>Type[0]</keyword>
 277           <keyword>CProp[0]</keyword>
 278           <keyword>Type[1]</keyword>
 279           <keyword>CProp[1]</keyword>
 280           <keyword>Type[2]</keyword>
 281           <keyword>CProp[2]</keyword>
 282         </context>
 283       </include>
 284     </context>
 285   </definitions>
 286
 287 <!--
 288   <pattern-item _name = "Command [" style = "Keyword">
 289     <regex>\[</regex>
 290   </pattern-item>
 291   <pattern-item _name = "Command |" style = "Keyword">
 292     <regex>\|</regex>
 293   </pattern-item>
 294   <pattern-item _name = "Command ]" style = "Keyword">
 295     <regex>\]</regex>
 296   </pattern-item>
 297   <pattern-item _name = "Command {" style = "Keyword">
 298     <regex>\{</regex>
 299   </pattern-item>
 300   <pattern-item _name = "Command }" style = "Keyword">
 301     <regex>\}</regex>
 302   </pattern-item>
 303   <pattern-item _name = "Notation ast mark" style = "Keyword">
 304     <regex>@</regex>
 305   </pattern-item>
 306   <pattern-item _name = "Notation meta mark" style = "Keyword">
 307     <regex>\$</regex>
 308   </pattern-item>
 309   -->
 310 </language>