real life implementation of the highlighting, added css

diff --git a/helm/www/matita/grafite-format.css b/helm/www/matita/grafite-format.css
new file mode 100644 (file)
index 0000000..a02229d
--- /dev/null
+++ b/helm/www/matita/grafite-format.css
@@ -0,0 +1,41 @@
+
+.grafite_TheoremKinds {
+       color: #7779bb;
+       font-weight: bold;
+}
+
+.grafite_Commands {
+       color: #200080;
+       font-weight: bold;
+}
+
+.grafite_Tactics {
+       color: #930000;
+       font-style: italic;
+}
+
+.grafite_Macros {
+       color: #004a43;
+}
+
+.grafite_Sorts {
+       color: #7779bb;
+}
+
+.grafite_Operators {
+       color: #44aadd;
+}
+
+.grafite_String {
+       color: #1060b6;
+}
+
+.grafite_Comment {
+       color: #595979;
+}
+
+.grafite_Symbols {
+       color: #406080;
+       font-weight: bold;
+}
+

diff --git a/helm/www/matita/grafite.hrc b/helm/www/matita/grafite.hrc
index 4b88fa91dc6b2f5707b918abbf77acc75f95f5e3..7ebf82f638dd967f2d0a0ec493192d02ca439b67 100644 (file)
--- a/helm/www/matita/grafite.hrc
+++ b/helm/www/matita/grafite.hrc
@@ -1,188 +1,179 @@
 <?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>&quot;</start-regex>
-    <end-regex>&quot;</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="/&#34;.*?&#34;/" region="String"/>
+
+    <block start="/\(\*/" end="/\*\)/" scheme="grafite-comment" region="Comment" />
+
+  </scheme>
+
+  <scheme name="grafite-comment">
+    <regexp match=".*" region="Comment" />
+  </scheme>
+
+ </type>
+</hrc>

diff --git a/helm/www/matita/helm-proto.hrc b/helm/www/matita/helm-proto.hrc
index f678424528e79a5e66e5172d58ea04c2ed7c7433..90b6235429c14872f5c9ba0072f8feeedf68945d 100644 (file)
--- a/helm/www/matita/helm-proto.hrc
+++ b/helm/www/matita/helm-proto.hrc
@@ -17,6 +17,8 @@
     <filename>/\.ma$/i</filename>
   </prototype>
 
-  <type name="default"><scheme name="grafite"/></type>
+  <type name="default">
+    <scheme name="grafite" />
+  </type>
 
 </hrc>

diff --git a/helm/www/matita/navy.css b/helm/www/matita/navy.css
new file mode 100644 (file)
index 0000000..335b372
--- /dev/null
+++ b/helm/www/matita/navy.css
@@ -0,0 +1,247 @@
+/* Generated with hrd2css.pl from ./Colorer-take5.beta4/hrd/rgb/navy.hrd */
+
+.def_HorzCross {
+       color: #000000;
+       background-color: #e8e7f8;
+}
+
+.def_VertCross {
+       color: #000000;
+       background-color: #e1e0f2;
+}
+
+.def_Number {
+       color: #008c00;
+}
+
+.def_NumberDec {
+       color: #008c00;
+}
+
+.def_NumberHex {
+       color: #008000;
+}
+
+.def_NumberBin {
+       color: #005b00;
+}
+
+.def_NumberOct {
+       color: #008c00;
+}
+
+.def_NumberFloat {
+       color: #008000;
+}
+
+.def_NumberSuffix {
+       color: #006600;
+}
+
+.def_String {
+       color: #1060b6;
+}
+
+.def_StringContent {
+       color: #0f69ff;
+}
+
+.def_StringEdge {
+       color: #800000;
+}
+
+.def_CharacterContent {
+       color: #0000cc;
+}
+
+.def_Comment {
+       color: #595979;
+}
+
+.def_CommentContent {
+       color: #7F9FBF;
+       font-weight: bold;
+}
+
+.def_CommentEdge {
+       color: #606090;
+}
+
+.def_CommentDoc {
+       color: #3F7F8F;
+}
+
+.def_CommentDocEdge {
+       color: #c0bd92;
+}
+
+.def_Symbol {
+       color: #308080;
+}
+
+.def_SymbolStrong {
+       color: #406080;
+}
+
+.def_Prefix {
+       color: #0066ee;
+}
+
+.def_Operator {
+       color: #44aadd;
+}
+
+.def_Keyword {
+       color: #200080;
+       font-weight: bold;
+}
+
+.def_KeywordStrong {
+       color: #7779bb;
+       font-weight: bold;
+}
+
+.def_FunctionKeyword {
+       color: #400000;
+}
+
+.def_DeprecatedKeyword {
+       color: #008484;
+}
+
+.def_InterfaceKeyword {
+       color: #008484;
+}
+
+.def_ClassKeyword {
+       color: #6679aa;
+       font-weight: bold;
+}
+
+.def_StructKeyword {
+       color: #003060;
+}
+
+.def_TypeKeyword {
+       color: #7779bb;
+}
+
+.def_Register {
+       color: #000080;
+}
+
+.def_Constant {
+       color: #7d0045;
+}
+
+.def_Var {
+       color: #007d45;
+}
+
+.def_VarStrong {
+       color: #007997;
+}
+
+.def_Identifier {
+       color: #005fd2;
+}
+
+.def_BooleanConstant {
+       color: #0f4d75;
+}
+
+.def_Directive {
+       color: #004a43;
+}
+
+.def_Parameter {
+       color: #074726;
+}
+
+.def_ParameterUnknown {
+       color: #474796;
+}
+
+.def_Tag {
+       color: #333385;
+}
+
+.def_OpenTag {
+       color: #0057a6;
+}
+
+.def_CloseTag {
+       color: #0057a6;
+}
+
+.def_Label {
+       color: #e34adc;
+}
+
+.def_LabelStrong {
+       color: #000000;
+       background-color: #a8a800;
+}
+
+.def_Insertion {
+       color: #000000;
+       background-color: #cceeee;
+}
+
+.def_Error {
+       color: #ffffff;
+       background-color: #dd9999;
+       font-weight: bold;
+       font-style: italic;
+}
+
+.def_ErrorText {
+       color: #ee00ee;
+}
+
+.def_TODO {
+       color: #ffffff;
+       background-color: #808000;
+}
+
+.def_Debug {
+       color: #80abfd;
+       background-color: #007084;
+}
+
+.def_Path {
+       color: #40015a;
+}
+
+.def_URL {
+       color: #5555DD;
+}
+
+.def_EMail {
+       color: #7144c4;
+}
+
+.def_Date {
+       color: #009797;
+}
+
+.def_Time {
+       color: #8745a0;
+}
+
+.def_PairStart {
+       color: #d0d0ff;
+}
+
+.def_PairEnd {
+       color: #d0d0ff;
+}
+
+.def_PairStrongStart {
+       color: #880088;
+}
+
+.def_PairStrongEnd {
+       color: #880088;
+}
+