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          <!-- objects -->
  79          <keyword>theorem</keyword>
  80          <keyword>record</keyword>
  81          <keyword>definition</keyword>
  82          <keyword>inductive</keyword>
  83          <keyword>coinductive</keyword>
  84          <keyword>let</keyword>
  85          <keyword>lemma</keyword>
  86          <keyword>remark</keyword>
  87          <keyword>axiom</keyword>
  88
  89          <!-- tactics -->
  90          <keyword>apply</keyword>
  91          <keyword>applyS</keyword>
  92          <keyword>cases</keyword>
  93          <keyword>letin</keyword>
  94          <keyword>auto</keyword>
  95          <keyword>elim</keyword>
  96          <keyword>whd</keyword>
  97          <keyword>normalize</keyword>
  98          <keyword>assumption</keyword>
  99          <keyword>generalize</keyword>
 100          <keyword>change</keyword>
 101          <keyword>rewrite</keyword>
 102          <keyword>cut</keyword>
 103          <keyword>inversion</keyword>
 104          <keyword>lapply</keyword>
 105          <keyword>destruct</keyword>
 106
 107           <!-- commands -->
 108           <keyword>alias</keyword>
 109           <keyword>and</keyword>
 110           <keyword>as</keyword>
 111           <keyword>coercion</keyword>
 112           <keyword>prefer</keyword>
 113           <keyword>nocomposites</keyword>
 114           <keyword>coinductive</keyword>
 115           <keyword>corec</keyword>
 116           <keyword>default</keyword>
 117           <keyword>discriminator</keyword>
 118           <keyword>for</keyword>
 119           <keyword>include</keyword>
 120           <keyword>include'</keyword>
 121           <keyword>inductive</keyword>
 122           <keyword>inverter</keyword>
 123           <keyword>in</keyword>
 124           <keyword>interpretation</keyword>
 125           <keyword>let</keyword>
 126           <keyword>match</keyword>
 127           <keyword>names</keyword>
 128           <keyword>notation</keyword>
 129           <keyword>on</keyword>
 130           <keyword>qed</keyword>
 131           <keyword>rec</keyword>
 132           <keyword>record</keyword>
 133           <keyword>return</keyword>
 134           <keyword>source</keyword>
 135           <keyword>to</keyword>
 136           <keyword>using</keyword>
 137           <keyword>with</keyword>
 138
 139
 140           <!-- commands -->
 141           <keyword>unification</keyword>
 142           <keyword>hint</keyword>
 143           <keyword>coercion</keyword>
 144           <keyword>inverter</keyword>
 145           <keyword>qed</keyword>
 146
 147           <!-- macros -->
 148           <keyword>check</keyword>
 149           <keyword>eval</keyword>
 150           <keyword>hint</keyword>
 151           <keyword>set</keyword>
 152           <keyword>auto</keyword>
 153           <keyword>nodefaults</keyword>
 154           <keyword>coercions</keyword>
 155           <keyword>comments</keyword>
 156           <keyword>debug</keyword>
 157
 158           <!-- tinycals -->
 159           <keyword>try</keyword>
 160           <keyword>solve</keyword>
 161           <keyword>do</keyword>
 162           <keyword>repeat</keyword>
 163           <keyword>first</keyword>
 164           <keyword>focus</keyword>
 165           <keyword>unfocus</keyword>
 166           <keyword>progress</keyword>
 167           <keyword>skip</keyword>
 168         </context>
 169         <context id="types" style-ref="type">
 170           <!-- sorts -->
 171           <keyword>Prop</keyword>
 172           <keyword>Type[0]</keyword>
 173           <keyword>CProp[0]</keyword>
 174           <keyword>Type[1]</keyword>
 175           <keyword>CProp[1]</keyword>
 176           <keyword>Type[2]</keyword>
 177           <keyword>CProp[2]</keyword>
 178         </context>
 179         <context id="quantifiers" style-ref="quantifiers">
 180           <!-- quantifiers -->
 181           <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
 182         </context>
 183         <context id="tinycals" style-ref="tinycals">
 184                 <match>\[|\||\]|\{|\}|>|//|&lt;|@|\$|#|\\\\|;|\.|:>|:|-</match>
 185         </context>
 186       </include>
 187     </context>
 188   </definitions>
 189 </language>