Prise en compte du repertoire dans le section path; utilisation de dirpath pour les noms de modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 18 insertions, 21 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 55c77b0769..5da2d9f357 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -41,9 +41,8 @@ let all_subdirs root =
   in
   if exists_dir root then
    begin
-    let root_base_name = Filename.basename root in
-     add root root_base_name ;
-     traverse root root_base_name
+     add root "";
+     traverse root ""
    end ;
   List.rev !l
 
diff --git a/lib/util.ml b/lib/util.ml
index dd5be58714..05b147cee3 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -32,28 +32,26 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
-let parse_section_path s =
+let check_is_ident s =
+  let len = String.length s in
+  if len = 0 then invalid_arg "parse_loadpath: is not a valid name";
+  (* TODO... *)
+  ()
+
+let parse_loadpath s =
   let len = String.length s in
   let rec decoupe_dirs n =
-    try
-      let pos = String.index_from s n '#' in
+    try  
+      let pos = String.index_from s n '/' in
+      if pos = n then
+	invalid_arg "parse_loadpath: find an empty dir in loadpath";
       let dir = String.sub s n (pos-n) in
-      let dirs,n' = decoupe_dirs (succ pos) in
-      dir::dirs,n'
-    with
-      | Not_found -> [],n
-  in
-  let decoupe_kind n =
-    try
-      let pos = String.index_from s n '.' in
-      String.sub s n (pos-n), String.sub s (succ pos) (pred (len-pos))
+      check_is_ident dir;
+      dir :: (decoupe_dirs (succ pos))
     with
-      | Not_found -> invalid_arg "parse_section_path"
+      | Not_found -> [String.sub s n (len-n)]
   in
-  if len = 0 || String.get s 0 <> '#' then invalid_arg "parse_section_path";
-  let dirs,n = decoupe_dirs 1 in
-  let id,k = decoupe_kind n in
-  dirs,id,k
+  if len = 0 then [] else decoupe_dirs 0
 
 module Stringset = Set.Make(struct type t = string let compare = compare end)
 
diff --git a/lib/util.mli b/lib/util.mli
index ed1ac8ee35..58e356c0d2 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -30,7 +30,7 @@ val invalid_arg_loc : loc * string -> 'a
 val explode : string -> string list
 val implode : string list -> string
 
-val parse_section_path : string -> string list * string * string
+val parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string