From 511cb2f5f42d80af9262b5cf7458a434cd652e95 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 14 Jan 2009 12:54:59 +0000
Subject: 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
---
 parsing/lexer.ml4 | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'parsing/lexer.ml4')

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;
-- 
cgit v1.2.3