erreurs lexicales

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

2 files changed, 13 insertions, 8 deletions

diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 982e294363..721afa2d1c 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,7 +1,12 @@
 
 (* $Id$ *)
 
-exception BadToken of string
+type error =
+  | Illegal_character
+  | Unterminated_comment
+  | Unterminated_string
+
+exception Error of error
 
 val add_keyword : string -> unit
 val is_keyword : string -> bool
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 680835499a..410bcc4fa6 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -9,9 +9,7 @@ type error =
   | Unterminated_comment
   | Unterminated_string
 
-exception BadToken of string
-
-exception Error of error * int * int
+exception Error of error
 
 (* token trees *)
 
@@ -157,6 +155,8 @@ rule token = parse
         token lexbuf }
   | eof 
       { ("EOI","") }
+  | _ { let loc = (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf) in
+	raise (Stdpp.Exc_located (loc, Error Illegal_character)) }
 
 and comment = parse
   | "(*"
@@ -178,8 +178,8 @@ and comment = parse
   | "'\\" ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
       { comment lexbuf }
   | eof
-      { raise (Error (Unterminated_comment,
-                      !comment_start_pos, !comment_start_pos+2)) }
+      { let loc = (!comment_start_pos, !comment_start_pos+2) in
+	raise (Stdpp.Exc_located (loc, Error Unterminated_comment)) }
   | _
       { comment lexbuf }
 
@@ -196,8 +196,8 @@ and string = parse
       { Buffer.add_char string_buffer (char_for_decimal_code lexbuf 1);
         string lexbuf }
   | eof
-      { raise (Error (Unterminated_string,
-                      !string_start_pos, !string_start_pos+1)) }
+      { let loc = (!string_start_pos, !string_start_pos+1) in
+	raise (Stdpp.Exc_located (loc, Error Unterminated_string)) }
   | _
       { Buffer.add_char string_buffer (Lexing.lexeme_char lexbuf 0);
         string lexbuf }