]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/matita1.0/grafite.hrc
Created a new directory for Matita1.0
[helm.git] / helm / www / matita1.0 / grafite.hrc
diff --git a/helm/www/matita1.0/grafite.hrc b/helm/www/matita1.0/grafite.hrc
new file mode 100644 (file)
index 0000000..7ebf82f
--- /dev/null
@@ -0,0 +1,179 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE hrc PUBLIC "-//Cail Lomecb//DTD Colorer HRC take5//EN"
+  "http://colorer.sf.net/2003/hrc.dtd">
+<hrc version="take5" xmlns="http://colorer.sf.net/2003/hrc"
+     xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+     xsi:schemaLocation="http://colorer.sf.net/2003/hrc http://colorer.sf.net/2003/hrc.xsd">
+
+ <type name="grafite">
+
+   <annotation>
+     <documentation>
+       Grafite: Matita scripts language
+     </documentation>
+   </annotation>
+
+  <region name="TheoremKinds" />
+  <region name="Commands" />
+  <region name="Tactics" />
+  <region name="Macros" />
+  <region name="Sorts" />
+  <region name="Operators" />
+  <region name="Symbols" />
+  <region name="Comment" />
+  <region name="String" />
+
+  <scheme name="grafite">
+
+    <keywords region="TheoremKinds" ignorecase="no">
+      <word name="theorem" />
+      <word name="definition" />
+      <word name="lemma" />
+      <word name="fact" />
+      <word name="remark" />
+      <word name="variant" />
+    </keywords>
+
+    <keywords region="Commands" ignorecase="no">
+      <word name="axiom" />
+      <word name="alias" />
+      <word name="and" />
+      <word name="as" />
+      <word name="coercion" />
+      <word name="coinductive" />
+      <word name="corec" />
+      <word name="default" />
+      <word name="for" />
+      <word name="include" />
+      <word name="include" />
+      <word name="inductive" />
+      <word name="in" />
+      <word name="interpretation" />
+      <word name="let" />
+      <word name="match" />
+      <word name="names" />
+      <word name="notation" />
+      <word name="on" />
+      <word name="qed" />
+      <word name="rec" />
+      <word name="record" />
+      <word name="return" />
+      <word name="to" />
+      <word name="using" />
+      <word name="with" />
+    </keywords>
+
+    <keywords region="Tactics" ignorecase="no">
+      <word name="absurd" />
+      <word name="apply" />
+      <word name="assumption" />
+      <word name="auto" />
+      <word name="paramodulation" />
+      <word name="clear" />
+      <word name="clearbody" />
+      <word name="change" />
+      <word name="constructor" />
+      <word name="contradiction" />
+      <word name="cut" />
+      <word name="decompose" />
+      <word name="discriminate" />
+      <word name="elim" />
+      <word name="elimType" />
+      <word name="exact" />
+      <word name="exists" />
+      <word name="fail" />
+      <word name="fold" />
+      <word name="fourier" />
+      <word name="fwd" />
+      <word name="generalize" />
+      <word name="goal" />
+      <word name="id" />
+      <word name="injection" />
+      <word name="intro" />
+      <word name="intros" />
+      <word name="inversion" />
+      <word name="lapply" />
+      <word name="linear" />
+      <word name="left" />
+      <word name="letin" />
+      <word name="normalize" />
+      <word name="reduce" />
+      <word name="reflexivity" />
+      <word name="replace" />
+      <word name="rewrite" />
+      <word name="ring" />
+      <word name="right" />
+      <word name="symmetry" />
+      <word name="simplify" />
+      <word name="split" />
+      <word name="to" />
+      <word name="transitivity" />
+      <word name="unfold" />
+      <word name="whd" />
+    </keywords>
+
+    <keywords region="Tactics" ignorecase="no">
+      <!-- tacticals -->
+      <word name="try" />
+      <word name="solve" />
+      <word name="do" />
+      <word name="repeat" />
+      <word name="first" />
+      <word name="focus" />
+      <word name="unfocus" />
+    </keywords>
+
+    <keywords region="Macros" ignorecase="no">
+      <word name="check" />
+      <word name="hint" />
+      <word name="set" />
+    </keywords>
+
+    <regexp match="/whelp\s+(elim|hint|instance|locate|match)/" region="Macros"/>
+
+    <keywords region="Sorts" ignorecase="no">
+      <word name="Set" />
+      <word name="Prop" />
+      <word name="Type" />
+    </keywords>
+
+    <keywords region="Operators" ignorecase="no">
+      <symb name="\def" />
+      <symb name="\forall" />
+      <symb name="\lambda" />
+      <symb name="\to" />
+      <symb name="\exists" />
+      <symb name="\Rightarrow" />
+      <symb name="\Assign" />
+      <symb name="\land" />
+      <symb name="\lor" />
+      <symb name="\lnot" />
+      <symb name="\liff" />
+      <symb name="\subst" />
+      <symb name="\vdash" />
+      <symb name="\iforall" />
+      <symb name="\iexists" />
+    </keywords>
+
+    <keywords region="Symbols" ignorecase="no">
+      <symb name="[" />
+      <symb name="]" />
+      <symb name="|" />
+      <symb name="{" />
+      <symb name="}" />
+      <symb name="@" />
+      <symb name="$" />
+    </keywords>
+
+    <regexp match="/&#34;.*?&#34;/" region="String"/>
+
+    <block start="/\(\*/" end="/\*\)/" scheme="grafite-comment" region="Comment" />
+
+  </scheme>
+
+  <scheme name="grafite-comment">
+    <regexp match=".*" region="Comment" />
+  </scheme>
+
+ </type>
+</hrc>