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.

1 files changed, 37 insertions, 22 deletions

diff --git a/ide/coq.lang b/ide/coq.lang
index e25eedbca..484264ece 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>