]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMisc.ml
removed no longer used METAs
[helm.git] / helm / matita / matitaMisc.ml
index e311973c9cc362c726d503839154c2efee644c0b..0c4329e554350936ea863f1c2e581e13df8ca5d9 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
-open MatitaTypes 
 
 (** Functions "imported" from Http_getter_misc *)
 
-let strip_trailing_slash = Http_getter_misc.strip_trailing_slash
 let normalize_dir = Http_getter_misc.normalize_dir
 let strip_suffix = Http_getter_misc.strip_suffix
 
-let baseuri_of_baseuri_decl st =
-  match st with
-  | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
-      Some buri
-  | _ -> None
-
-let is_empty buri =
- List.for_all
-  (function
-      Http_getter_types.Ls_section _ -> true
-    | 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 +142,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
@@ -195,4 +150,3 @@ let list_tl_at ?(equality=(==)) e l =
     | hd :: tl -> aux tl
   in
   aux l
-