From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 library/library.ml | 53 +++++++++++++++++++++++++++++------------------------
 1 file changed, 29 insertions(+), 24 deletions(-)

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index 760b6f07..cfd88ca0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: library.ml 8877 2006-05-30 16:37:04Z notin $ *)
 
 open Pp
 open Util
@@ -57,7 +57,6 @@ let canonical_path_name p =
     (* We give up to find a canonical name and just simplify it... *)
     strip_path p
 
-
 let find_logical_path phys_dir = 
   let phys_dir = canonical_path_name phys_dir in
   match list_filter2 (fun p d -> p = phys_dir) !load_paths with
@@ -65,38 +64,44 @@ let find_logical_path phys_dir =
   | _,[] -> Nameops.default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
+let is_in_load_paths phys_dir =
+  let dir = canonical_path_name phys_dir in
+  let lp = get_load_paths () in
+  let check_p = fun p -> (String.compare dir p) == 0 in
+    List.exists check_p lp 
+
 let remove_load_path dir =
   load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
 let add_load_path (phys_path,coq_path) =
   let phys_path = canonical_path_name phys_path in
-  match list_filter2 (fun p d -> p = phys_path) !load_paths with
-  | _,[dir] ->
-      if coq_path <> dir 
-        (* If this is not the default -I . to coqtop *)
-        && not
-        (phys_path = canonical_path_name Filename.current_dir_name
-         && coq_path = Nameops.default_root_prefix)
-      then
-	begin
-          (* Assume the user is concerned by library naming *)
-	  if dir <> Nameops.default_root_prefix then
-	    (Options.if_verbose warning (phys_path^" was previously bound to "
-	    ^(string_of_dirpath dir)
-	    ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
-             flush_all ());
-	  remove_load_path phys_path;
-	  load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
-	end
-  | _,[] ->
-      load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
-  | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+    match list_filter2 (fun p d -> p = phys_path) !load_paths with
+      | _,[dir] ->
+	  if coq_path <> dir 
+            (* If this is not the default -I . to coqtop *)
+            && not
+            (phys_path = canonical_path_name Filename.current_dir_name
+		&& coq_path = Nameops.default_root_prefix)
+	  then
+	    begin
+              (* Assume the user is concerned by library naming *)
+	      if dir <> Nameops.default_root_prefix then
+		(Options.if_verbose warning (phys_path^" was previously bound to "
+					     ^(string_of_dirpath dir)
+					     ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
+		 flush_all ());
+	      remove_load_path phys_path;
+	      load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+	    end
+      | _,[] ->
+	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+      | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let physical_paths (dp,lp) = dp
 
 let load_paths_of_dir_path dir =
   fst (list_filter2 (fun p d -> d = dir) !load_paths)
-
+    
 let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
 
 (************************************************************************)
-- 
cgit v1.2.3