Coqide: revised parsing of coq sentences

 In particular, grouping { and } delimiters is now allowed.
 The only place where blank (i.e. space or newline or eof) is mandatory
 is after dots. For instance "{{tac. }{tac. }}" is ok, while
 "tac.}" is not seen as containing any sentence delimiter but rather
 the inner-sentence token ".}", that might have been registered (or not)
 to Coq by the user via some tactic or constr notation.

 This way, coqide should be in sync with what is accepted by coqtop.
 Current cvs version of proofgeneral is slightly more laxist, but
 this will probably be harmonized soon.

 Technically, we cannot rely anymore on functions like
 forward_to_tag_toggle, since two delimiters "}}" could be adjacent,
 hence no toogle of the corresponding tag. Instead, we use a simplier
 (less efficient ?) iterative search.

 When retagging a zone after some edition, we retag up to a real "."
 delimiter (or eof), since the status of "{" "}" as delimiters is
 too fragile to be trusted after edition.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14394 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index a88c94dac..e937e9875 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -75,7 +75,7 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let ident = firstchar identchar*
 
-let undotted_sep = [ '{' '}' ] (space | eof)
+let undotted_sep = [ '{' '}' ]
 
 let dot_sep = '.' (space | eof)