fixed two preblems in matitadep, one coming from the dep-parser and

the other one from a wrong path normalization routine

diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml
index 53d8c74e878b4f511877116160a4a74661a29a29..3ee270e4e00b42fd0b012a512b11a92feef48c82 100644 (file)
--- a/components/extlib/hExtlib.ml
+++ b/components/extlib/hExtlib.ml
@@ -425,14 +425,14 @@ let estimate_size x =
 let normalize_path s = 
   let s = Str.global_replace (Str.regexp "//") "/" s in
   let l = Str.split (Str.regexp "/") s in
-  let rec aux = function
-    | [] -> []
-    | he::".."::tl -> aux tl
-    | he::"."::tl -> aux (he::tl)
-    | he::tl -> he :: aux tl
+  let rec aux acc = function
+    | [] -> acc
+    | he::"."::tl -> aux acc (he::tl)
+    | he::".."::tl when he <> ".." -> aux [] (acc @ tl)
+    | he::tl -> aux (acc@[he]) tl
   in
   (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^
-  String.concat "/" (aux l)
+  String.concat "/" (aux [] l)
   ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "")
 ;;
 
@@ -444,7 +444,8 @@ let find_in paths path =
        try
          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
          else aux tl
-       with Unix.Unix_error _ -> aux tl
+       with Unix.Unix_error _ as exn -> 
+               aux tl
    in
    try
      aux paths

diff --git a/components/grafite_parser/dependenciesParser.ml b/components/grafite_parser/dependenciesParser.ml
index 360cdb14d0998b98c83be19c18565f8d7ce6e5b2..2f7c5ec0cffbfdd2138bba285c6bfa3646ca896a 100644 (file)
--- a/components/grafite_parser/dependenciesParser.ml
+++ b/components/grafite_parser/dependenciesParser.ml
@@ -53,6 +53,8 @@ let parse_dependencies lexbuf =
         parse (UriDep (UriManager.uri_of_string u) :: acc)
     | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
         parse (IncludeDep fname :: acc)
+    | [< '("IDENT", "include'"); '("QSTRING", fname) >] ->
+        parse (IncludeDep fname :: acc)
     | [< '("EOI", _) >] -> acc
     | [< 'tok >] -> parse acc
     | [<  >] -> acc) tok_stream

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index f2268488f2afbc3ce975578c072a172af1ec72ac..cc3c96999453a8e88d1b42560c550acc347f3a0e 100644 (file)
--- a/components/library/librarian.ml
+++ b/components/library/librarian.ml
@@ -52,7 +52,7 @@ let find_root_for ~include_paths file =
  try 
    let path = HExtlib.find_in include_paths file in
    let path = absolutize path in
-   (* HLog.debug ("file "^file^" resolved as "^path); *)
+(*     HLog.debug ("file "^file^" resolved as "^path);  *)
    let rootpath, root, buri = 
      try
        let mburi = Helm_registry.get "matita.baseuri" in
@@ -65,12 +65,13 @@ let find_root_for ~include_paths file =
        let buri = List.assoc "baseuri" (load_root_file rootpath) in
        rootpath, Filename.dirname rootpath, buri
    in
-   (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
+(*     HLog.debug ("file "^file^" rooted by "^rootpath^"");  *)
    let uri = Http_getter_misc.strip_trailing_slash buri in
    if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
      HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
    ensure_trailing_slash root, remove_trailing_slash uri, path
  with Failure "find_in" -> 
+   HLog.error ("We are in: " ^ Sys.getcwd ());
    HLog.error ("Unable to find: "^file^"\nPaths explored:");
    List.iter (fun x -> HLog.error (" - "^x)) include_paths;
    raise (NoRootFor file)