<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE language SYSTEM "language.dtd">
-<language _name="grafite" version="1.0" _section="Sources" mimetypes="text/x-matita">
-
- <escape-char>\</escape-char>
-
- <block-comment _name = "Commented Code" style = "Comment">
- <start-regex>\(\*\*[^\)]</start-regex>
- <end-regex>[^\(]\*\*\)</end-regex>
- </block-comment>
-
- <block-comment _name = "Block Comment" style = "Comment">
- <start-regex>\(\*</start-regex>
- <end-regex>\*\)</end-regex>
- </block-comment>
-
- <keyword-list _name = "Theorem Kinds" style = "Keyword" case-sensitive="TRUE">
- <keyword>theorem</keyword>
- <keyword>definition</keyword>
- <keyword>lemma</keyword>
- <keyword>fact</keyword>
- <keyword>remark</keyword>
- <keyword>variant</keyword>
- <keyword>axiom</keyword>
- </keyword-list>
-
- <keyword-list _name = "Commands" style = "Keyword" case-sensitive="TRUE">
- <keyword>alias</keyword>
- <keyword>and</keyword>
- <keyword>as</keyword>
- <keyword>coercion</keyword>
- <keyword>coinductive</keyword>
- <keyword>corec</keyword>
- <keyword>default</keyword>
- <keyword>for</keyword>
- <keyword>include</keyword>
- <keyword>include'</keyword>
- <keyword>inductive</keyword>
- <keyword>in</keyword>
- <keyword>interpretation</keyword>
- <keyword>let</keyword>
- <keyword>match</keyword>
- <keyword>names</keyword>
- <keyword>notation</keyword>
- <keyword>on</keyword>
- <keyword>qed</keyword>
- <keyword>rec</keyword>
- <keyword>record</keyword>
- <keyword>return</keyword>
- <keyword>to</keyword>
- <keyword>using</keyword>
- <keyword>with</keyword>
- </keyword-list>
-
- <pattern-item _name = "Command [" style = "Keyword">
- <regex>\[</regex>
- </pattern-item>
- <pattern-item _name = "Command |" style = "Keyword">
- <regex>\|</regex>
- </pattern-item>
- <pattern-item _name = "Command ]" style = "Keyword">
- <regex>\]</regex>
- </pattern-item>
- <pattern-item _name = "Command {" style = "Keyword">
- <regex>\{</regex>
- </pattern-item>
- <pattern-item _name = "Command }" style = "Keyword">
- <regex>\}</regex>
- </pattern-item>
- <pattern-item _name = "Notation ast mark" style = "Keyword">
- <regex>@</regex>
- </pattern-item>
- <pattern-item _name = "Notation meta mark" style = "Keyword">
- <regex>\$</regex>
- </pattern-item>
-
- <keyword-list _name = "Sorts" style = "Data Type" case-sensitive="TRUE">
- <keyword>Set</keyword>
- <keyword>Prop</keyword>
- <keyword>Type</keyword>
- </keyword-list>
-
- <keyword-list _name = "Tactics" style = "Others 2" case-sensitive="TRUE">
- <keyword>absurd</keyword>
- <keyword>apply</keyword>
- <keyword>assumption</keyword>
- <keyword>auto</keyword>
- <keyword>paramodulation</keyword>
- <keyword>clear</keyword>
- <keyword>clearbody</keyword>
- <keyword>change</keyword>
- <keyword>constructor</keyword>
- <keyword>contradiction</keyword>
- <keyword>cut</keyword>
- <keyword>decompose</keyword>
- <keyword>discriminate</keyword>
- <keyword>elim</keyword>
- <keyword>elimType</keyword>
- <keyword>exact</keyword>
- <keyword>exists</keyword>
- <keyword>fail</keyword>
- <keyword>fold</keyword>
- <keyword>fourier</keyword>
- <keyword>fwd</keyword>
- <keyword>generalize</keyword>
- <keyword>goal</keyword>
- <keyword>id</keyword>
- <keyword>injection</keyword>
- <keyword>intro</keyword>
- <keyword>intros</keyword>
- <keyword>inversion</keyword>
- <keyword>lapply</keyword>
- <keyword>linear</keyword>
- <keyword>left</keyword>
- <keyword>letin</keyword>
- <keyword>normalize</keyword>
- <keyword>reduce</keyword>
- <keyword>reflexivity</keyword>
- <keyword>replace</keyword>
- <keyword>rewrite</keyword>
- <keyword>ring</keyword>
- <keyword>right</keyword>
- <keyword>symmetry</keyword>
- <keyword>simplify</keyword>
- <keyword>split</keyword>
- <keyword>to</keyword>
- <keyword>transitivity</keyword>
- <keyword>unfold</keyword>
- <keyword>whd</keyword>
- </keyword-list>
-
- <keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
- <keyword>try</keyword>
- <keyword>solve</keyword>
- <keyword>do</keyword>
- <keyword>repeat</keyword>
- <keyword>first</keyword>
- <keyword>focus</keyword>
- <keyword>unfocus</keyword>
- </keyword-list>
-
-
- <keyword-list _name = "Matita Macro" style = "Others 3" case-sensitive="TRUE">
- <keyword>check</keyword>
- <keyword>hint</keyword>
- <keyword>set</keyword>
- </keyword-list>
-
- <keyword-list _name = "Whelp Macro" style = "Others 3"
- case-sensitive="TRUE"
- beginning-regex="whelp *"
- match-empty-string-at-beginning="FALSE"
- match-empty-string-at-end="FALSE" >
- <keyword>elim</keyword>
- <keyword>hint</keyword>
- <keyword>instance</keyword>
- <keyword>locate</keyword>
- <keyword>match</keyword>
- </keyword-list>
-
- <keyword-list _name = "TeX Macro" style = "Preprocessor"
- case-sensitive="TRUE"
- beginning-regex="\\"
- match-empty-string-at-beginning="FALSE"
- match-empty-string-at-end="FALSE" >
- <keyword>def</keyword>
- <keyword>forall</keyword>
- <keyword>lambda</keyword>
- <keyword>to</keyword>
- <keyword>exists</keyword>
- <keyword>Rightarrow</keyword>
- <keyword>Assign</keyword>
- <keyword>land</keyword>
- <keyword>lor</keyword>
- <keyword>lnot</keyword>
- <keyword>liff</keyword>
- <keyword>subst</keyword>
- <keyword>vdash</keyword>
- <keyword>iforall</keyword>
- <keyword>iexists</keyword>
- </keyword-list>
-
- <string _name = "String" style = "String" >
- <start-regex>"</start-regex>
- <end-regex>"</end-regex>
- </string>
-
-</language>
+<!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="/".*?"/" region="String"/>
+
+ <block start="/\(\*/" end="/\*\)/" scheme="grafite-comment" region="Comment" />
+
+ </scheme>
+
+ <scheme name="grafite-comment">
+ <regexp match=".*" region="Comment" />
+ </scheme>
+
+ </type>
+</hrc>
projects / helm.git / blobdiff