erreurs lexicales

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

5 files changed, 39 insertions, 21 deletions

diff --git a/Makefile b/Makefile
index 05659ece6..df332485f 100644
--- a/Makefile
+++ b/Makefile
@@ -111,12 +111,12 @@ CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \
 CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx)
 
 ###########################################################################
-# Main targets
+# Main targets (coqmktop, coqtop, coqtop.byte)
 ###########################################################################
 
 COQMKTOP=scripts/coqmktop
 
-world: minicoq coqtop.byte $(COQMKTOP) dev/db_printers.cmo
+world: $(COQMKTOP) coqtop.byte coqtop states tools
 
 coqtop: $(COQMKTOP) $(CMX)
 	$(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop
@@ -156,12 +156,20 @@ toplevel: $(TOPLEVEL)
 
 # states
 
+states: states/barestate.coq
+
 SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPMultipleCase.v
 
 states/barestate.coq: $(SYNTAXPP) coqtop.byte
 	./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
 
 ###########################################################################
+# tools
+###########################################################################
+
+tools: dev/db_printers.cmo
+
+###########################################################################
 # minicoq
 ###########################################################################
 
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 982e29436..721afa2d1 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 680835499..410bcc4fa 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 }
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 4d2a44262..c64498904 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -37,21 +37,22 @@ let load_rcfile() =
        raise e)
   else mSGNL [< 'sTR"Skipping rcfile loading." >]
 
-(*Puts dir in the path of ML and in the LoadPath*)
+(* Puts dir in the path of ML and in the LoadPath *)
 let add_include s =
   Mltop.dir_ml_dir s;
   add_path s
 
-(*By the option -include -I or -R of the command line*)
+(* By the option -include -I or -R of the command line *)
 let includes = ref []
 let push_include s = includes := s :: !includes
-let rec_include s = includes := (all_subdirs s)@(!includes)
+let rec_include s = includes := (all_subdirs s) @ !includes
 
-(*Because find puts "./" and the loadpath is not really pretty-printed*)
-let hm2 str=
-  String.sub str 2 ((String.length str)-2)
+(* Because find puts "./" and the loadpath is not nicely pretty-printed *)
+let hm2 s = 
+  let n = String.length s in
+  if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s
 
-(*Initializes the LoadPath according to COQLIB and Coq_config*)
+(* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
   (* default load path; only if COQLIB is defined *)
   begin
@@ -62,18 +63,15 @@ let init_load_path () =
 	  (fun s -> add_include (Filename.concat coqlib s))
       	  ("states" :: 
 	   (List.map (fun s -> Filename.concat "theories" (hm2 s))
-             Coq_config.theories_dirs))
+              Coq_config.theories_dirs))
     with Not_found -> ()
   end ;
-
   begin
     try
       let camlp4 = Sys.getenv "CAMLP4LIB" in add_include camlp4
     with Not_found -> ()
   end ;
-
   add_include "." ;
-
   (* additional loadpath, given with -I -include -R options *)
   List.iter add_include (List.rev !includes);
   includes := []
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 444d18b42..af8b7c5cb 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -6,6 +6,7 @@ open Util
 open Ast
 open Inductive
 open Type_errors
+open Lexer
 
 let print_loc loc =
   if loc = dummy_loc then 
@@ -55,6 +56,12 @@ let rec explain_exn_default = function
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
                else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
                explain_exn_default exc >]
+
+  | Lexer.Error Illegal_character -> [< 'sTR "Illegal character." >]
+	
+  | Lexer.Error Unterminated_comment -> [< 'sTR "Unterminated comment." >]
+	
+  | Lexer.Error Unterminated_string -> [< 'sTR "Unterminated string." >]
 	
   | reraise ->
       flush_all();