diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 50 |
1 files changed, 35 insertions, 15 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 0b6d93d6..b6690fe4 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Flags @@ -45,12 +45,12 @@ open System to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *) (* This path is where we look for .cmo *) -let coq_mlpath_copy = ref ["."] +let coq_mlpath_copy = ref [Sys.getcwd ()] let keep_copy_mlpath path = let cpath = CUnix.canonical_path_name path in - let filter path' = not (String.equal cpath (CUnix.canonical_path_name path')) + let filter path' = not (String.equal cpath path') in - coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy + coq_mlpath_copy := cpath :: List.filter filter !coq_mlpath_copy (* If there is a toplevel under Coq *) type toplevel = { @@ -118,8 +118,8 @@ let ml_load s = | WithTop t -> (try t.load_obj s; s with - | e when Errors.noncritical e -> - let e = Errors.push e in + | e when CErrors.noncritical e -> + let e = CErrors.push e in match fst e with | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) | exc -> @@ -146,7 +146,12 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> msg_warning (str "Cannot access the ML compiler") + | _ -> + let moreinfo = + if Dynlink.is_native then " Loading ML code works only in bytecode." + else "" + in + errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) (* Adds a path to the ML paths *) let add_ml_dir s = @@ -155,19 +160,31 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path *) +(* For Rec Add ML Path (-R) *) let add_rec_ml_dir unix_path = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) (* Adding files to Coq and ML loadpath *) +let warn_cannot_use_directory = + CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" + (fun d -> + str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)") + let convert_string d = try Names.Id.of_string d with UserError _ -> - msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); + warn_cannot_use_directory d; raise Exit -let add_rec_path ~unix_path ~coq_root ~implicit = +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> str "Cannot open " ++ str unix_path) + +type add_ml = AddNoML | AddTopML | AddRecML + +let add_rec_path add_ml ~unix_path ~coq_root ~implicit = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in let prefix = Names.DirPath.repr coq_root in @@ -178,13 +195,16 @@ let add_rec_path ~unix_path ~coq_root ~implicit = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let () = add_ml_dir unix_path in + let () = match add_ml with + | AddNoML -> () + | AddTopML -> add_ml_dir unix_path + | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in let add (path, dir) = Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - msg_warning (str "Cannot open " ++ str unix_path) + warn_cannot_open_path unix_path (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -324,10 +344,10 @@ let if_verbose_load verb f name ?path fname = let info = str "[Loading ML file " ++ str fname ++ str " ..." in try let path = f name ?path fname in - msg_info (info ++ str " done]"); + Feedback.msg_info (info ++ str " done]"); path with reraise -> - msg_info (info ++ str " failed]"); + Feedback.msg_info (info ++ str " failed]"); raise reraise (** Load a module for the first time (i.e. dynlink it) @@ -391,7 +411,7 @@ let inMLModule : ml_module_object -> obj = let declare_ml_modules local l = let l = List.map mod_of_name l in - Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) + Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = let l = !coq_mlpath_copy in |