diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-14 12:54:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-14 12:54:59 +0000 |
| commit | 511cb2f5f42d80af9262b5cf7458a434cd652e95 (patch) | |
| tree | 1ea8c93c8dc668079fedfc32eb7df6696fa51c30 /parsing/lexer.ml4 | |
| parent | 7aea5b4a925f752c8e056d2ca1e9bfe48a066372 (diff) | |
Fixing #1960 (xml bug with external on goal variable) and #1961
(anomaly while parsing $ not followed by an ident).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11785 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/lexer.ml4')
| -rw-r--r-- | parsing/lexer.ml4 | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5984f7415..045c2ecca 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -372,6 +372,16 @@ let process_chars bp c cs = | Some t -> (("", t), (bp, ep)) | None -> err (bp, ep) Undefined_token +let parse_after_dollar bp = + parser + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> + ("METAIDENT", get_buff len) + | [< s >] -> + match lookup_utf8 s with + | Utf8Token (UnicodeLetter, n) -> + ("METAIDENT", get_buff (ident_tail (nstore n 0 s) s)) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '$' s) + (* Parse what follows a dot *) let parse_after_dot bp c = parser @@ -399,10 +409,8 @@ let parse_after_qmark bp s = let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c) >] ep -> - comment_stop bp; - (("METAIDENT", get_buff len), (bp,ep)) + | [< ''$'; t = parse_after_dollar bp >] ep -> + comment_stop bp; (t, (ep, bp)) | [< ''.' as c; t = parse_after_dot bp c >] ep -> comment_stop bp; if Flags.do_beautify() & t=("",".") then between_com := true; |