X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=e311973c9cc362c726d503839154c2efee644c0b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=97d6cac4738b2b0a12c53ceaaad7cfc99d19dda5;hpb=8ecc9fb74f80c2f5b3e3c70f0a625e63a48292fb;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 97d6cac47..e311973c9 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -38,39 +38,6 @@ let baseuri_of_baseuri_decl st = Some buri | _ -> None -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Stream.of_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 @@ -80,29 +47,28 @@ let is_empty buri = let safe_remove fname = if Sys.file_exists fname then Sys.remove fname -let is_dir fname = - try - (Unix.stat fname).Unix.st_kind = Unix.S_DIR - with Unix.Unix_error _ -> false - -let is_regular fname = - try - (Unix.stat fname).Unix.st_kind = Unix.S_REG - with Unix.Unix_error _ -> false - -let input_file fname = - let size = (Unix.stat fname).Unix.st_size in - let buf = Buffer.create size in - let ic = open_in fname in - Buffer.add_channel buf ic size; - close_in ic; - Buffer.contents buf - -let output_file data file = - let oc = open_out file in - output_string oc data; - close_out oc - +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 @@ -116,45 +82,6 @@ let append_phrase_sep s = else s -let mkdir path = - let components = Str.split (Str.regexp "/") path in - let rec aux where = function - | [] -> () - | piece::tl -> - let path = where ^ "/" ^ piece in - (try - Unix.mkdir path 0o755 - with - | Unix.Unix_error (Unix.EEXIST,_,_) -> () - | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e))); - aux path tl - in - aux "" components - -let trim_blanks = - let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in - fun s -> (Pcre.extract ~rex s).(1) - -let split ?(char = ' ') s = - let pieces = ref [] in - let rec aux idx = - match (try Some (String.index_from s idx char) with Not_found -> None) with - | Some pos -> - pieces := String.sub s idx (pos - idx) :: !pieces; - aux (pos + 1) - | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces - in - aux 0; - List.rev !pieces - -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 *) @@ -249,36 +176,6 @@ 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 unopt = function None -> failwith "unopt: None" | Some v -> v - let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n let end_ma_RE = Pcre.regexp "\\.ma$" @@ -290,17 +187,6 @@ let obj_file_of_baseuri 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 @@ -310,9 +196,3 @@ let list_tl_at ?(equality=(==)) e l = in aux l -let debug_wrap name f = - prerr_endline (sprintf "debug_wrap: ==>> %s" name); - let res = f () in - prerr_endline (sprintf "debug_wrap: <<== %s" name); - res -