diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 20 | ||||
| -rw-r--r-- | toplevel/errors.ml | 7 |
2 files changed, 16 insertions, 11 deletions
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(); |