X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.lang;h=9238684a08cc4de408bd86aef9bfeb85bbee2bb5;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=a1d578b6d1c0f4dd91e085b9e47cf14c847ae44c;hpb=5f3a6dbe686146cc7176130aa295bd603338cac2;p=helm.git

diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index a1d578b6d..9238684a0 100644
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -9,17 +9,18 @@
 
   <styles>
     <style id="comment" _name="Comment" map-to="def:comment"/>
-    <style id="base-n-integer" _name="Base-N Integer" map-to="def:base-n-integer"/>
     <style id="string" _name="String" map-to="def:string"/>
+    <style id="escape" _name="Escape" map-to="def:string"/>
     <style id="keyword" _name="Keyword" map-to="def:keyword"/>
     <style id="type" _name="Data Type" map-to="def:type"/>
-    <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
+    <style id="latex" _name="LaTeX Escaped" map-to="def:special-char"/>
+    <style id="macros" _name="Macros" map-to="def:keyword"/>
+    <style id="tinycals" _name="Tinycals" map-to="def:keyword"/>
+    <style id="quantifiers" _name="Quantifiers" map-to="def:type"/>
   </styles>
 
   <definitions>
-    <define-regex id="cap-ident">\b[A-Z][A-Za-z0-9_']*</define-regex>
-    <define-regex id="low-ident">\b[a-z][A-Za-z0-9_']*</define-regex>
-    <define-regex id="char-esc">\\((\\|"|'|n|t|b|r)|[0-9]{3}|x[0-9a-fA-F]{2})</define-regex>
+    <define-regex id="char-esc">\\"|[0-9a-zA-Z]</define-regex>
     <context id="escape-seq" style-ref="escape">
       <match>\%{char-esc}</match>
     </context>
@@ -53,6 +54,32 @@
 	<context id="character-constant" style-ref="string">
 	  <match>('\%{char-esc}')|('[^\\']')</match>
 	</context>
+	<context id="whelp_macros" style-ref="macros">
+	 <prefix>whelp *</prefix>
+         <keyword>elim</keyword>
+         <keyword>hint</keyword>
+         <keyword>instance</keyword>
+         <keyword>locate</keyword>
+         <keyword>match</keyword>
+	</context>
+	<context id="latex" style-ref="latex">
+	 <prefix>\\</prefix>
+         <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>
+	</context>
 	<!-- Flow control & common keywords -->
 	<context id="keywords" style-ref="keyword">
 	 <!-- objects -->
@@ -72,6 +99,7 @@
          <keyword>ncoinductive</keyword>
          <keyword>nlet</keyword>
          <keyword>nlemma</keyword>
+         <keyword>nremark</keyword>
          <keyword>naxiom</keyword>
 
          <!-- tactics -->
@@ -155,6 +183,7 @@
 
          <!-- ntactics -->
          <keyword>napply</keyword>	    	 
+         <keyword>napplyS</keyword>	    	 
          <keyword>ncases</keyword>	    	 
          <keyword>nletin</keyword>	    	 
          <keyword>nauto</keyword>	    	 
@@ -166,6 +195,7 @@
          <keyword>nchange</keyword>	    	 
          <keyword>nrewrite</keyword>	    	 
          <keyword>ncut</keyword>	    	 
+         <keyword>ninversion</keyword>
          <keyword>nlapply</keyword>
          <keyword>ndestruct</keyword> 
 
@@ -252,66 +282,14 @@
           <keyword>Type[2]</keyword>
           <keyword>CProp[2]</keyword>
 	</context>
+        <context id="quantifiers" style-ref="quantifiers">
+          <!-- quantifiers -->
+          <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
+        </context>
+        <context id="tinycals" style-ref="tinycals">
+          <match>\[|\||\]|\{|\}|@|\$|#|\\\\|;|\.|:>|:</match>
+        </context>
       </include>
     </context>
   </definitions>
-
-<!--
-  <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 = "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>
-  -->
 </language>