]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/grafite.hrc
...
[helm.git] / 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>