]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarian.ml
get rid of gragrep, matitamake(Lib) and development windows,
[helm.git] / components / library / librarian.ml
index e8d0e7da12120e7672282c7e1c9fa68314e2498d..417035a8138d36a118e2cf0d65bdcc7e05936034 100644 (file)
@@ -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^""); *)