From 8a257c7d5f10cd7939611c7bb10be5415f4cc887 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 7 Jul 2011 15:16:30 +0000
Subject: Coqide understand { and }

It doesn't use them for indenting.
Worst, the undo around "End ..." bug leaks on '}' !

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14267 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq_lex.mll | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'ide/coq_lex.mll')

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 2ce8777c3..51e0610bc 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -83,6 +83,8 @@ let ident = firstchar identchar*
 
 let sentence_sep = '.' [ ' ' '\r' '\n' '\t' ]
 
+let undotted_command = [ '{' '}' ]
+
 let multiword_declaration =
   "Module" (space+ "Type")?
 | "Program" space+ ident
@@ -185,6 +187,13 @@ and sentence stamp = parse
       sentence stamp lexbuf }
   | ".."
   | _    { sentence stamp lexbuf}
+  | undotted_command space? { (* the space? here is a awful consequence of
+				 the way lexing is asked by Coqide.split_slice_lax:
+				 a training whitespace is add at the end of text
+				 and then dropped. This space has consequently to be
+				 part of the sentence *)
+      if not !start then sentence stamp lexbuf (* in the middle of a command our token
+						  aren't command *)}
   | sentence_sep { }
   | eof { raise Not_found }
 
-- 
cgit v1.2.3