From 5725e4913f1759596e6ab63ea05cc6ed439041ec Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 9 Aug 2011 16:58:24 +0000 Subject: 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 --- ide/coq_lex.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide/coq_lex.mll') 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) -- cgit v1.2.3