diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_prim.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 15 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 24 |
3 files changed, 22 insertions, 19 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index c24534e2d..524e7b468 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 2276800d5..809e5bec3 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 d7fa2b575..ba128be5f 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 |