From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 toplevel/mltop.ml | 50 +++++++++++++++++++++++++++++++++++---------------
 1 file changed, 35 insertions(+), 15 deletions(-)

(limited to 'toplevel/mltop.ml')

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
-- 
cgit v1.2.3