irediced usage of matita.includes, that is now set by

[helm.git] / components / library / librarian.ml

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index e8d0e7da12120e7672282c7e1c9fa68314e2498d..5918136764b6816c5b54dc5a2435d1093fdf02f9 100644 (file)
--- a/components/library/librarian.ml
+++ b/components/library/librarian.ml
@@ -22,6 +22,18 @@ let remove_trailing_slash s =
   if s.[len-1] = '/' then String.sub s 0 (len-1) else s
 ;;
 
+let parse_root rootpath =
+  let data = HExtlib.input_file rootpath in
+  let lines = Str.split (Str.regexp "\n") data in
+  List.map 
+    (fun l -> 
+      match Str.split (Str.regexp "=") l with
+      | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v
+      | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
+    lines
+;;
+
+
 let find_root_for ~include_paths file = 
  let include_paths = "" :: Sys.getcwd () :: include_paths in
  let path = HExtlib.find_in include_paths file in
@@ -35,18 +47,7 @@ let find_root_for ~include_paths file =
      | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
    with Helm_registry.Key_not_found "matita.baseuri" -> 
      let rootpath = find_root path in
-     let data = HExtlib.input_file rootpath in
-     let buri = 
-       let lines = Str.split (Str.regexp "\n") data in
-       let lines = 
-         List.map (fun l -> 
-           match Str.split (Str.regexp "=") l with
-           | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v
-           | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
-           lines
-       in
-       List.assoc "baseuri" lines
-     in
+     let buri = List.assoc "baseuri" (parse_root rootpath) in
      rootpath, Filename.dirname rootpath, buri
  in
  (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
@@ -55,7 +56,7 @@ let find_root_for ~include_paths file =
    HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
  ensure_trailing_slash root, remove_trailing_slash uri, path
 ;;
-  
+
 let baseuri_of_script ?(include_paths=[]) file = 
   let root, buri, path = find_root_for ~include_paths file in
   let path = HExtlib.normalize_path path in
@@ -74,10 +75,12 @@ let baseuri_of_script ?(include_paths=[]) file =
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in
+  let extra = String.concat "/" extra_buri in
    root,
    remove_trailing_slash (HExtlib.normalize_path 
-    (buri ^ "/" ^ chop (String.concat "/" extra_buri))),
-   path
+    (buri ^ "/" ^ chop extra)),
+   path,
+   extra
 ;;
 
 let find_roots_in_dir dir =