From 24f3c342457119ed2a7936fdaacce30221f07aef Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 17 Sep 2014 15:27:54 +0200
Subject: Fix broken syntax highlighting for Coq files using "Proof constr".

See Eqdep_dec.v for instance. Module declarations were not highlighted
because the IDE wrongly believed they were used inside an unterminated
proof.
---
 ide/coq.lang | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'ide/coq.lang')

diff --git a/ide/coq.lang b/ide/coq.lang
index 1950b81a3..656041d30 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -116,7 +116,7 @@
 	  </include>
 	</context>
 	<context id="proof">
-	  <start>Proof</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"/>
@@ -142,6 +142,15 @@
 	    </context>
 	  </include>
 	</context>
+	<context id="exact-proof">
+	  <start>Proof</start>
+	  <end>\%{dot_sep}</end>
+	  <include>
+	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
+	    <context ref="constr-keyword"/>
+	    <context ref="constr-sort"/>
+	  </include>
+	</context>
 	<context id="undotted-sep" style-ref="vernac-keyword">
 	  <match>\%{undotted_sep}</match>
 	</context>
-- 
cgit v1.2.3