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
 129           <!-- commands -->
 130           <keyword>alias</keyword>
 131           <keyword>and</keyword>
 132           <keyword>as</keyword>
 133           <keyword>associative</keyword>
 134           <keyword>coercion</keyword>
 135           <keyword>prefer</keyword>
 136           <keyword>nocomposites</keyword>
 137           <keyword>coinductive</keyword>
 138           <keyword>constraint</keyword>
 139           <keyword>corec</keyword>
 140           <keyword>cyclic</keyword>
 141           <keyword>default</keyword>
 142           <keyword>discriminator</keyword>
 143           <keyword>for</keyword>
 144           <keyword>id</keyword>
 145           <keyword>include</keyword>
 146           <keyword>include'</keyword>
 147           <keyword>inductive</keyword>
 148           <keyword>inverter</keyword>
 149           <keyword>in</keyword>
 150           <keyword>interpretation</keyword>
 151           <keyword>left</keyword>
 152           <keyword>let</keyword>
 153           <keyword>match</keyword>
 154           <keyword>names</keyword>
 155           <keyword>non</keyword>
 156           <keyword>notation</keyword>
 157           <keyword>on</keyword>
 158           <keyword>precedence</keyword>
 159           <keyword>qed</keyword>
 160           <keyword>defined</keyword>
 161           <keyword>rec</keyword>
 162           <keyword>record</keyword>
 163           <keyword>return</keyword>
 164           <keyword>right</keyword>
 165           <keyword>source</keyword>
 166           <keyword>symbol</keyword>
 167           <keyword>to</keyword>
 168           <keyword>universe</keyword>
 169           <keyword>using</keyword>
 170           <keyword>with</keyword>
 171
 172
 173           <!-- commands -->
 174           <keyword>unification</keyword>
 175           <keyword>hint</keyword>
 176           <keyword>coercion</keyword>
 177           <keyword>inverter</keyword>
 178           <keyword>qed</keyword>
 179
 180           <!-- macros -->
 181           <keyword>check</keyword>
 182           <keyword>eval</keyword>
 183           <keyword>hint</keyword>
 184           <keyword>set</keyword>
 185           <keyword>auto</keyword>
 186           <keyword>nodefaults</keyword>
 187           <keyword>coercions</keyword>
 188           <keyword>comments</keyword>
 189           <keyword>debug</keyword>
 190
 191           <!-- tinycals -->
 192           <keyword>try</keyword>
 193           <keyword>solve</keyword>
 194           <keyword>do</keyword>
 195           <keyword>repeat</keyword>
 196           <keyword>first</keyword>
 197           <keyword>focus</keyword>
 198           <keyword>unfocus</keyword>
 199           <keyword>progress</keyword>
 200           <keyword>skip</keyword>
 201         </context>
 202         <context id="types" style-ref="type">
 203           <!-- sorts -->
 204           <keyword>Prop</keyword>
 205           <keyword>Type[0]</keyword>
 206           <keyword>CProp[0]</keyword>
 207           <keyword>Type[1]</keyword>
 208           <keyword>CProp[1]</keyword>
 209           <keyword>Type[2]</keyword>
 210           <keyword>CProp[2]</keyword>
 211         </context>
 212         <context id="quantifiers" style-ref="quantifiers">
 213           <!-- quantifiers -->
 214           <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
 215         </context>
 216         <context id="tinycals" style-ref="tinycals">
 217                 <match>\[|\||\]|\{|\}|>|//|&lt;|@|\$|#|\\\\|;|\.|:>|:|-</match>
 218         </context>
 219       </include>
 220     </context>
 221   </definitions>
 222 </language>