The lexer is changer to break former PATTERNIDENT into two tokens.

This allows more flexibility in the other uses of the question mark
and in particular suppresses the hack for rewriter in g_tactic.ml4


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

3 files changed, 22 insertions, 19 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index c24534e2df..524e7b4681 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -45,7 +45,7 @@ GEXTEND Gram
     [ [ s = IDENT -> id_of_string s ] ]
   ;
   pattern_ident:
-    [ [ s = PATTERNIDENT -> id_of_string s ] ]
+    [ [ s = LEFTQMARK; id = ident -> id ] ]
   ;
   pattern_identref:
     [ [ id = pattern_ident -> (loc, id) ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2276800d53..809e5bec35 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -435,19 +435,10 @@ GEXTEND Gram
     [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
   ;
   rewriter : 
-    [ [ 
-    (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally 
-       produce a pattern_ident *)
-        c = pattern_ident -> 
-	  let c = (CRef (Ident (loc,c)), NoBindings) in  
-	  (RepeatStar, c)
-      | n = natural; c = pattern_ident -> 
-	  let c = (CRef (Ident (loc,c)), NoBindings) in  
-	  (UpTo n, c)
-      | "!"; c = constr_with_bindings -> (RepeatPlus,c)
-      |	"?"; c = constr_with_bindings -> (RepeatStar,c)
+    [ [ "!"; c = constr_with_bindings -> (RepeatPlus,c)
+      | ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c)
       | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
-      |	n = natural; "?"; c = constr_with_bindings -> (UpTo n,c)
+      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings -> (UpTo n,c)
       | n = natural; c = constr_with_bindings -> (Precisely n,c)
       | c = constr_with_bindings -> (Precisely 1, c)
       ] ]
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index d7fa2b5753..ba128be5f3 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -175,7 +175,7 @@ let add_keyword str =
 (* Adding a new token (keyword or special token). *)
 let add_token (con, str) = match con with
   | "" -> add_keyword str
-  | "METAIDENT" | "PATTERNIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
+  | "METAIDENT" | "LEFTQMARK" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
       -> ()
   | _ ->
       raise (Token.Error ("\
@@ -372,19 +372,29 @@ let process_chars bp c cs =
     | Some t -> (("", t), (bp, ep))
     | None -> err (bp, ep) Undefined_token
 
-(* Parse what follows a dot/question mark *)
+(* Parse what follows a dot *)
 let parse_after_dot bp c =
-  let constructor = if c = '?' then "PATTERNIDENT" else "FIELD" in
   parser
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ->
-      (constructor, get_buff len)
+      ("FIELD", get_buff len)
   | [< s >] ->
       match lookup_utf8 s with
       | Utf8Token (UnicodeLetter, n) -> 
-	  (constructor, get_buff (ident_tail (nstore n 0 s) s))
+	  ("FIELD", get_buff (ident_tail (nstore n 0 s) s))
       | AsciiChar | Utf8Token _ | EmptyStream -> 
 	  fst (process_chars bp c s)
 
+(* Parse what follows a question mark *)
+let parse_after_qmark bp s =
+  match Stream.peek s with
+    |Some ('a'..'z' | 'A'..'Z') -> ("LEFTQMARK", "")
+    |None -> ("","?")
+    | _ ->
+	match lookup_utf8 s with
+	  | Utf8Token (UnicodeLetter, _) -> ("LEFTQMARK", "")
+	  | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '?' s)
+
+
 (* Parse a token in a char stream *)
 let rec next_token = parser bp
   | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
@@ -393,10 +403,12 @@ let rec next_token = parser bp
       len = ident_tail (store 0 c) >] ep -> 
       comment_stop bp;
       (("METAIDENT", get_buff len), (bp,ep))
-  | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep ->
+  | [< ''.' as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
       if Flags.do_translate() & t=("",".") then between_com := true;
       (t, (bp,ep))
+  | [< ''?'; s >] ep ->
+      let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
        len = ident_tail (store 0 c) >] ep ->
       let id = get_buff len in