From 5bcccd7ed80acdb9904d5a623f1aba42183803a4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 28 Apr 2016 20:38:07 +0200
Subject: Make the language grammar much more precise. (Fix bugs #4682 and
 #4683)

Rather than being isolated words, commands and tactics now extend till
dot separators. So bullets can be defined as living only at the top level
of proofs, which should make their detection much more robust.
---
 ide/coq.lang | 59 +++++++++++++++++++++++++++++++++++++----------------------
 1 file changed, 37 insertions(+), 22 deletions(-)

diff --git a/ide/coq.lang b/ide/coq.lang
index e25eedbca9..484264ece3 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -95,11 +95,24 @@
       <keyword>Type</keyword>
     </context>
 
-    <context id="coq" class="no-spell-check">
+    <!-- Terms -->
+    <context id="constr">
       <include>
         <context ref="string"/>
         <context ref="coqdoc"/>
         <context ref="comment"/>
+        <context ref="constr-sort"/>
+        <context ref="constr-keyword"/>
+        <context id="dot-nosep">
+          <match>\.\.</match>
+        </context>
+      </include>
+    </context>
+
+    <context id="coq" class="no-spell-check">
+      <include>
+        <context ref="coqdoc"/>
+        <context ref="comment"/>
 
         <context id="declaration">
           <start>\%{decl_head}</start>
@@ -110,14 +123,7 @@
             <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
             <context sub-pattern="id_list" where="start" style-ref="identifier"/>
             <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
-            <context ref="constr-keyword"/>
-            <context ref="constr-sort"/>
-            <context id="dot-nosep">
-              <match>\.\.</match>
-            </context>
-            <context ref="string"/>
-            <context ref="coqdoc"/>
-            <context ref="comment"/>
+            <context ref="constr"/>
           </include>
         </context>
 
@@ -127,21 +133,19 @@
           <include>
             <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
             <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
-            <context ref="command-in-proof"/>
-            <context ref="string"/>
             <context ref="coqdoc"/>
             <context ref="comment"/>
-            <context ref="constr-keyword"/>
-            <context ref="constr-sort"/>
-            <context id="bullet" extend-parent="false">
-              <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match>
+            <context id="bullet" style-ref="vernac-keyword" extend-parent="false">
+              <match>\%{bullet}</match>
+            </context>
+            <context extend-parent="false">
+              <start>\%[</start>
+              <end>\%{dot_sep}</end>
               <include>
-                <context sub-pattern="bul" style-ref="vernac-keyword"/>
+                <context ref="command-in-proof"/>
+                <context ref="constr"/>
               </include>
             </context>
-            <context id="bullet-sol" style-ref="vernac-keyword">
-              <match>^\s*\%{bullet}</match>
-            </context>
           </include>
         </context>
 
@@ -150,11 +154,19 @@
           <end>\%{dot_sep}</end>
           <include>
             <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-            <context ref="constr-keyword"/>
-            <context ref="constr-sort"/>
+            <context ref="constr"/>
           </include>
         </context>
 
+        <context ref="command"/>
+      </include>
+    </context>
+
+    <!-- Toplevel commands -->
+    <context id="command" extend-parent="false">
+      <start>\%[</start>
+      <end>\%{dot_sep}</end>
+      <include>
         <context id="command-in-proof" style-ref="vernac-keyword">
           <keyword>About</keyword>
           <keyword>Check</keyword>
@@ -166,7 +178,7 @@
           <keyword>Transparent</keyword>
         </context>
 
-        <context id="command" style-ref="vernac-keyword">
+        <context id="toplevel-command" style-ref="vernac-keyword">
           <keyword>Add</keyword>
           <keyword>Load</keyword>
           <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
@@ -228,7 +240,10 @@
             <context sub-pattern="qua_list" style-ref="identifier"/>
           </include>
         </context>
+
+        <context ref="constr"/>
       </include>
     </context>
+
   </definitions>
 </language>
-- 
cgit v1.2.3