X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=389ee2325683336d020ab506e88fea298e4861e5;hb=b92a0ec32215eea5e0452154da54d5a29a84a53e;hp=e86e4b9a051e33ecfc81ab671b25cc7bd4359c48;hpb=d7c24dbca4f5e2baef606669db70cc640c02d38d;p=helm.git

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index e86e4b9a0..389ee2325 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -24,85 +24,12 @@
  *)
 
 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 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
-              MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
-            (try 
-              ignore(Http_getter.resolve u)
-            with
-            | Http_getter_types.Unresolvable_URI _ -> 
-                MatitaLog.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 _ as exn ->
-          prerr_endline ("Unable to parse: " ^ file);
-          prerr_endline (MatitaExcPp.to_string exn);
-          ()
-    done
-  with End_of_file -> close_in ic);
-  match !uri with
-  | Some uri -> uri
-  | None -> failwith ("No baseuri defined in " ^ file)
-
-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
   
@@ -115,14 +42,6 @@ let append_phrase_sep s =
   else
     s
 
-let empty_mathml () =
-  DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
-    ~qualifiedName:(Gdome.domString "math") ~doctype:None
-
-let empty_boxml () =
-  DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) 
-    ~qualifiedName:(Gdome.domString "box") ~doctype:None
-
 exception History_failure
 
 type 'a memento = 'a array * int * int * int  (* data, hd, tl, cur *)
@@ -217,56 +136,10 @@ let singleton f =
   let instance = lazy (f ()) in
   fun () -> Lazy.force instance
 
-let get_proof_status status =
-  match status.proof_status with
-  | Incomplete_proof s -> s
-  | _ -> statement_error "no ongoing proof"
-
-let get_proof_metasenv status =
-  match status.proof_status with
-  | No_proof -> []
-  | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv
-  | Proof (_, metasenv, _, _) -> metasenv
-  | Intermediate m -> m
-
-let get_proof_context status =
-  match status.proof_status with
-  | Incomplete_proof ((_, metasenv, _, _), goal) ->
-      let (_, context, _) = CicUtil.lookup_meta goal metasenv in
-      context
-  | _ -> []
- 
-let get_proof_conclusion status =
-  match status.proof_status with
-  | Incomplete_proof ((_, metasenv, _, _), goal) ->
-      let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
-      conclusion
-  | _ -> statement_error "no ongoing proof"
- 
-let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
-
 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 obj_file_of_script f =
- if f = "coq.ma" then BuildTimeConf.coq_notation_script else
-  let baseuri = baseuri_of_file f in
-   obj_file_of_baseuri baseuri
-
-let rec list_uniq = function 
-  | [] -> []
-  | h::[] -> [h]
-  | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
-  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
-
 let list_tl_at ?(equality=(==)) e l =
   let rec aux =
     function
@@ -275,4 +148,3 @@ let list_tl_at ?(equality=(==)) e l =
     | hd :: tl -> aux tl
   in
   aux l
-