diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 36c16208c..acd8026f9 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -146,7 +146,12 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> Feedback.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 = @@ -161,12 +166,22 @@ let add_rec_ml_dir 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 _ -> - Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); + warn_cannot_use_directory d; raise Exit +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> str "Cannot open " ++ str unix_path) + let add_rec_path ~unix_path ~coq_root ~implicit = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in @@ -184,7 +199,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - Feedback.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 = |