helm/www/matita/grafite.hrc

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <!DOCTYPE hrc PUBLIC "-//Cail Lomecb//DTD Colorer HRC take5//EN"
   3   "http://colorer.sf.net/2003/hrc.dtd">
   4 <hrc version="take5" xmlns="http://colorer.sf.net/2003/hrc"
   5      xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
   6      xsi:schemaLocation="http://colorer.sf.net/2003/hrc http://colorer.sf.net/2003/hrc.xsd">
   7
   8  <type name="grafite">
   9
  10    <annotation>
  11      <documentation>
  12        Grafite: Matita scripts language
  13      </documentation>
  14    </annotation>
  15
  16   <region name="TheoremKinds" />
  17   <region name="Commands" />
  18   <region name="Tactics" />
  19   <region name="Macros" />
  20   <region name="Sorts" />
  21   <region name="Operators" />
  22   <region name="Symbols" />
  23   <region name="Comment" />
  24   <region name="String" />
  25
  26   <scheme name="grafite">
  27
  28     <keywords region="TheoremKinds" ignorecase="no">
  29       <word name="theorem" />
  30       <word name="definition" />
  31       <word name="lemma" />
  32       <word name="fact" />
  33       <word name="remark" />
  34       <word name="variant" />
  35     </keywords>
  36
  37     <keywords region="Commands" ignorecase="no">
  38       <word name="axiom" />
  39       <word name="alias" />
  40       <word name="and" />
  41       <word name="as" />
  42       <word name="coercion" />
  43       <word name="coinductive" />
  44       <word name="corec" />
  45       <word name="default" />
  46       <word name="for" />
  47       <word name="include" />
  48       <word name="include" />
  49       <word name="inductive" />
  50       <word name="in" />
  51       <word name="interpretation" />
  52       <word name="let" />
  53       <word name="match" />
  54       <word name="names" />
  55       <word name="notation" />
  56       <word name="on" />
  57       <word name="qed" />
  58       <word name="rec" />
  59       <word name="record" />
  60       <word name="return" />
  61       <word name="to" />
  62       <word name="using" />
  63       <word name="with" />
  64     </keywords>
  65
  66     <keywords region="Tactics" ignorecase="no">
  67       <word name="absurd" />
  68       <word name="apply" />
  69       <word name="assumption" />
  70       <word name="auto" />
  71       <word name="paramodulation" />
  72       <word name="clear" />
  73       <word name="clearbody" />
  74       <word name="change" />
  75       <word name="constructor" />
  76       <word name="contradiction" />
  77       <word name="cut" />
  78       <word name="decompose" />
  79       <word name="discriminate" />
  80       <word name="elim" />
  81       <word name="elimType" />
  82       <word name="exact" />
  83       <word name="exists" />
  84       <word name="fail" />
  85       <word name="fold" />
  86       <word name="fourier" />
  87       <word name="fwd" />
  88       <word name="generalize" />
  89       <word name="goal" />
  90       <word name="id" />
  91       <word name="injection" />
  92       <word name="intro" />
  93       <word name="intros" />
  94       <word name="inversion" />
  95       <word name="lapply" />
  96       <word name="linear" />
  97       <word name="left" />
  98       <word name="letin" />
  99       <word name="normalize" />
 100       <word name="reduce" />
 101       <word name="reflexivity" />
 102       <word name="replace" />
 103       <word name="rewrite" />
 104       <word name="ring" />
 105       <word name="right" />
 106       <word name="symmetry" />
 107       <word name="simplify" />
 108       <word name="split" />
 109       <word name="to" />
 110       <word name="transitivity" />
 111       <word name="unfold" />
 112       <word name="whd" />
 113     </keywords>
 114
 115     <keywords region="Tactics" ignorecase="no">
 116       <!-- tacticals -->
 117       <word name="try" />
 118       <word name="solve" />
 119       <word name="do" />
 120       <word name="repeat" />
 121       <word name="first" />
 122       <word name="focus" />
 123       <word name="unfocus" />
 124     </keywords>
 125
 126     <keywords region="Macros" ignorecase="no">
 127       <word name="check" />
 128       <word name="hint" />
 129       <word name="set" />
 130     </keywords>
 131
 132     <regexp match="/whelp\s+(elim|hint|instance|locate|match)/" region="Macros"/>
 133
 134     <keywords region="Sorts" ignorecase="no">
 135       <word name="Set" />
 136       <word name="Prop" />
 137       <word name="Type" />
 138     </keywords>
 139
 140     <keywords region="Operators" ignorecase="no">
 141       <symb name="\def" />
 142       <symb name="\forall" />
 143       <symb name="\lambda" />
 144       <symb name="\to" />
 145       <symb name="\exists" />
 146       <symb name="\Rightarrow" />
 147       <symb name="\Assign" />
 148       <symb name="\land" />
 149       <symb name="\lor" />
 150       <symb name="\lnot" />
 151       <symb name="\liff" />
 152       <symb name="\subst" />
 153       <symb name="\vdash" />
 154       <symb name="\iforall" />
 155       <symb name="\iexists" />
 156     </keywords>
 157
 158     <keywords region="Symbols" ignorecase="no">
 159       <symb name="[" />
 160       <symb name="]" />
 161       <symb name="|" />
 162       <symb name="{" />
 163       <symb name="}" />
 164       <symb name="@" />
 165       <symb name="$" />
 166     </keywords>
 167
 168     <regexp match="/&#34;.*?&#34;/" region="String"/>
 169
 170     <block start="/\(\*/" end="/\*\)/" scheme="grafite-comment" region="Comment" />
 171
 172   </scheme>
 173
 174   <scheme name="grafite-comment">
 175     <regexp match=".*" region="Comment" />
 176   </scheme>
 177
 178  </type>
 179 </hrc>