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(-)

(limited to 'ide')

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


From bd5da52c6c625cb4559dd92051384383473ecb1b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 29 Apr 2016 17:01:05 +0200
Subject: Reduce ide/coq.png to 256x256.

Commit 1774a87 increased the file to 1024x1024. This had two adverse
consequences. First, the icon was too large to be used as a window icon
("gdk_window_set_icon_list: icons too large"), so Coqide 8.5 no longer had
an icon at runtime. Second, the file was also used in the About message
box, which was thus exceeding the display size of any reasonably-priced
device. This commit reverts the file to a saner size (still larger than
the original 66x100 picture).
---
 ide/coq.png | Bin 71924 -> 12907 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.png b/ide/coq.png
index cccd5a9a19..136bfdd5fe 100644
Binary files a/ide/coq.png and b/ide/coq.png differ
-- 
cgit v1.2.3