From 0b660db0a7d771ee8e165327cb954013bbc1a7c8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 6 Mar 2015 17:16:33 +0100
Subject: Simplify grammar for syntax highlighting by removing extraneous
 parentheses.

---
 ide/coq.lang | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'ide/coq.lang')

diff --git a/ide/coq.lang b/ide/coq.lang
index 22f0e48dc..38dabda50 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -22,19 +22,19 @@
   </styles>
   
   <definitions>
-    <define-regex id="space">\s</define-regex>
+    <define-regex id="space">\s+</define-regex>
     <define-regex id="first_ident_char">[_\p{L}]</define-regex>
     <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
     <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="undotted_sep">[-+*{}]</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
-    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion)</define-regex>
-    <define-regex id="mult_decl">(Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(Implicit\%{space}+Type(s)?)</define-regex>
-    <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
-    <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
-    <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)|(Save)</define-regex>
-    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal)</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
+    <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
+    <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
+    <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
+    <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex>
+    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
 
     <context id="escape-seq" style-ref="escape">
       <match>""</match>
@@ -112,7 +112,7 @@
 	  </include>
 	</context>
 	<context id="proof">
-	  <start>Proof(\%{dot_sep}|\%{space}+(using)|\%{space}+(with))</start>
+	  <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start>
 	  <end>\%{end_proof}\%{dot_sep}</end>
 	  <include>
 	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
@@ -159,15 +159,15 @@
 	  <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
 	  <keyword>Print</keyword>
 	  <keyword>Comments</keyword>
-	  <keyword>Solve\%{space}+Obligation</keyword>
-	  <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword>
-	  <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
+	  <keyword>Solve\%{space}Obligation</keyword>
+	  <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
+	  <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
 	  <keyword>\%{locality}Infix</keyword>
-	  <keyword>Declare\%{space}+ML\%{space}+Module</keyword>
-	  <keyword>Extraction\%{space}+Language\%{space}+(Ocaml|Haskell|Scheme)</keyword>
+	  <keyword>Declare\%{space}ML\%{space}Module</keyword>
+	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme)</keyword>
 	</context>
 	<context id="hint-command" style-ref="vernac-keyword">
-	  <prefix>\%{locality}Hint\%{space}+</prefix>
+	  <prefix>\%{locality}Hint\%{space}</prefix>
 	  <keyword>Resolve</keyword>
 	  <keyword>Immediate</keyword>
 	  <keyword>Constructors</keyword>
@@ -178,38 +178,38 @@
 	  <keyword>Rewrite</keyword>
 	</context>
 	<context id="scope-command" style-ref="vernac-keyword">
-	  <suffix>\%{space}+Scope</suffix>
+	  <suffix>\%{space}Scope</suffix>
 	  <keyword>\%{locality}Open</keyword>
 	  <keyword>\%{locality}Close</keyword>
 	  <keyword>Bind</keyword>
 	  <keyword>Delimit</keyword>
 	</context>
 	<context id="command-for-qualit">
-	  <suffix>\%{space}+(?'qua'\%{qualit})</suffix>
+	  <suffix>\%{space}(?'qua'\%{qualit})</suffix>
 	  <keyword>Chapter</keyword>
-	  <keyword>Combined\%{space}+Scheme</keyword>
-	  <keyword>Scheme\%{space}((Induction)|(Minimality)|(Elimination)|(Case)|(Equality))\%{space}for</keyword>
+	  <keyword>Combined\%{space}Scheme</keyword>
+	  <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword>
 	  <keyword>End</keyword>
 	  <keyword>Section</keyword>
-	  <keyword>Module(\%{space}+Type)?</keyword>
-	  <keyword>Declare\%{space}+Module(\%{space}+((Import)|(Export)))?</keyword>
+	  <keyword>Module(\%{space}Type)?</keyword>
+	  <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword>
 	  <keyword>About</keyword>
 	  <keyword>Arguments</keyword>
-	  <keyword>Implicit\%{space}+Arguments</keyword>
+	  <keyword>Implicit\%{space}Arguments</keyword>
 	  <keyword>Include</keyword>
-	  <keyword>Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive))</keyword>
+	  <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
 	  <include>
 	    <context sub-pattern="1" style-ref="vernac-keyword"/>
 	    <context sub-pattern="qua" style-ref="identifier"/>
 	  </include>
 	</context>
 	<context id="command-for-qualit-list">
-	  <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix>
+	  <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix>
 	  <keyword>Typeclasses (Transparent|Opaque)</keyword>
-	  <keyword>Require(\%{space}+((Import)|(Export)))?</keyword>
+	  <keyword>Require(\%{space}(Import|Export))?</keyword>
 	  <keyword>Import</keyword>
 	  <keyword>Export</keyword>
-	  <keyword>((Recursive|Separate)\%{space}+)?Extraction(\%{space}+(Library|(No)?Inline|Blacklist))?</keyword>
+	  <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
 	  <include>
 	    <context sub-pattern="1" style-ref="vernac-keyword"/>
 	    <context sub-pattern="qua_list" style-ref="identifier"/>
-- 
cgit v1.2.3