* Part of matita that used to deal with the library moved into ocaml/library

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index e311973c9cc362c726d503839154c2efee644c0b..077809a17bc5eaac26d001878b116102f650e808 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -45,31 +45,6 @@ let is_empty buri =
     | Http_getter_types.Ls_object _ -> false)
   (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
 
-let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
-
-let is_dir_empty d =
-  try 
-    let od = Unix.opendir d in
-    try 
-      ignore (Unix.readdir od);
-      ignore (Unix.readdir od);
-      ignore (Unix.readdir od);
-      Unix.closedir od;
-      false
-    with End_of_file -> 
-      Unix.closedir od;
-      true
-  with Unix.Unix_error _ -> true
-
-let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
-
-let rec rmdir_descend d = 
-  if is_dir_empty d then
-    begin
-      safe_rmdir d;
-      rmdir_descend (Filename.dirname d)
-    end
-
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
   
@@ -180,13 +155,6 @@ let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
 
 let end_ma_RE = Pcre.regexp "\\.ma$"
 
-let obj_file_of_baseuri baseuri =
- let path =
-  Helm_registry.get "matita.basedir" ^ "/xml" ^
-   Pcre.replace ~pat:"^cic:" ~templ:"" baseuri
- in
-  path ^ ".moo"
-
 let list_tl_at ?(equality=(==)) e l =
   let rec aux =
     function
@@ -196,3 +164,41 @@ let list_tl_at ?(equality=(==)) e l =
   in
   aux l
 
+let baseuri_of_file file = 
+  let uri = ref None in
+  let ic = open_in file in
+  let istream = Ulexing.from_utf8_channel ic in
+  (try
+    while true do
+      try 
+        let stm = GrafiteParser.parse_statement istream in
+        match baseuri_of_baseuri_decl stm with
+        | Some buri -> 
+            let u = strip_trailing_slash buri in
+            if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+              HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+            (try 
+              ignore(Http_getter.resolve u)
+            with
+            | Http_getter_types.Unresolvable_URI _ -> 
+                HLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+            | Http_getter_types.Key_not_found _ -> ());
+            uri := Some u;
+            raise End_of_file
+        | None -> ()
+      with
+        CicNotationParser.Parse_error err ->
+          HLog.error ("Unable to parse: " ^ file);
+          HLog.error ("Parse error: " ^ err);
+          ()
+    done
+  with End_of_file -> close_in ic);
+  match !uri with
+  | Some uri -> uri
+  | None -> failwith ("No baseuri defined in " ^ file)
+
+let obj_file_of_script ~basedir f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+  let baseuri = baseuri_of_file f in
+   LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
+