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="escape" _name="Escaped Character" map-to="def:special-char"/>
  17   </styles>
  18
  19   <definitions>
  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>
  25     </context>
  26     <!-- here's the main context -->
  27     <context id="grafite">
  28       <include>
  29         <context id="comment" style-ref="comment">
  30           <start>\(\*</start>
  31           <end>\*\)</end>
  32           <include>
  33             <context ref="string"/>
  34             <context id="comment-in-comment" style-ref="comment">
  35               <start>\(\*</start>
  36               <end>\*\)</end>
  37               <include>
  38                 <context ref="string"/>
  39                 <context ref="comment-in-comment"/>
  40                 <context ref="def:in-comment:*"/>
  41               </include>
  42             </context>
  43             <context ref="def:in-comment:*"/>
  44           </include>
  45         </context>
  46         <context id="string" style-ref="string">
  47           <start>"</start>
  48           <end>"</end>
  49           <include>
  50             <context ref="escape-seq"/>
  51           </include>
  52         </context>
  53         <context id="character-constant" style-ref="string">
  54           <match>('\%{char-esc}')|('[^\\']')</match>
  55         </context>
  56         <!-- Flow control & common keywords -->
  57         <context id="keywords" style-ref="keyword">
  58          <!-- objects -->
  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>
  66
  67          <!-- nobjects -->
  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>
  76
  77          <!-- tactics -->
  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>
 155
 156          <!-- ntactics -->
 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>
 171
 172           <!-- commands -->
 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>
 202
 203
 204           <!-- ncommands -->
 205           <keyword>unification</keyword>
 206           <keyword>hint</keyword>
 207           <keyword>ncoercion</keyword>
 208           <keyword>ninverter</keyword>
 209           <keyword>nqed</keyword>
 210
 211           <!-- macros -->
 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>
 224
 225           <!-- nmacros -->
 226           <keyword>ncheck</keyword>
 227
 228           <!-- tinycals -->
 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>
 238         </context>
 239         <context id="types" style-ref="type">
 240           <!-- sorts -->
 241           <keyword>Set</keyword>
 242           <keyword>Prop</keyword>
 243           <keyword>Type</keyword>
 244           <keyword>CProp</keyword>
 245
 246           <!-- nsorts -->
 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>
 254         </context>
 255       </include>
 256     </context>
 257   </definitions>
 258
 259 <!--
 260   <pattern-item _name = "Command [" style = "Keyword">
 261     <regex>\[</regex>
 262   </pattern-item>
 263   <pattern-item _name = "Command |" style = "Keyword">
 264     <regex>\|</regex>
 265   </pattern-item>
 266   <pattern-item _name = "Command ]" style = "Keyword">
 267     <regex>\]</regex>
 268   </pattern-item>
 269   <pattern-item _name = "Command {" style = "Keyword">
 270     <regex>\{</regex>
 271   </pattern-item>
 272   <pattern-item _name = "Command }" style = "Keyword">
 273     <regex>\}</regex>
 274   </pattern-item>
 275   <pattern-item _name = "Notation ast mark" style = "Keyword">
 276     <regex>@</regex>
 277   </pattern-item>
 278   <pattern-item _name = "Notation meta mark" style = "Keyword">
 279     <regex>\$</regex>
 280   </pattern-item>
 281
 282
 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>
 293   </keyword-list>
 294
 295   <keyword-list _name = "TeX Macro" style = "Preprocessor"
 296     case-sensitive="TRUE"
 297     beginning-regex="\\"
 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>
 315   </keyword-list>
 316   -->
 317 </language>