X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=389ee2325683336d020ab506e88fea298e4861e5;hb=4b07c19a0976a0928faf199c96cdf3edbfdaf0c6;hp=3ed1f001c2d17f5c2b185362b71f1fd0f0e443a8;hpb=b8c0504c5602b08443cec0782670bd4a699cbc23;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 3ed1f001c..389ee2325 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -24,83 +24,11 @@ *) open Printf -open MatitaTypes -let strip_trailing_slash = - let rex = Pcre.regexp "/$" in - fun s -> Pcre.replace ~rex s - -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 = 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 - 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 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 +(** Functions "imported" from Http_getter_misc *) +let normalize_dir = Http_getter_misc.normalize_dir +let strip_suffix = Http_getter_misc.strip_suffix let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file @@ -114,30 +42,6 @@ let append_phrase_sep s = else s -let strip_trailing_blanks = - let rex = Pcre.regexp "\\s*$" in - fun s -> Pcre.replace ~rex s - -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 *) @@ -232,74 +136,15 @@ let singleton f = let instance = lazy (f ()) in fun () -> Lazy.force instance -let mkdir d = - let errmsg = sprintf "Unable to create directory \"%s\"" d in - try - let dir = "mkdir -p " ^ d in - (match Unix.system dir with - | Unix.WEXITED 0 -> () - | Unix.WEXITED n -> - MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n); - failwith errmsg - | Unix.WSIGNALED s - | Unix.WSTOPPED s -> - MatitaLog.error - ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s); - failwith errmsg) - with Unix.Unix_error _ as exc -> - MatitaLog.error - ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc)); - failwith errmsg - -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_aliases status = status.aliases - -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$" -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 = - 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 debug_wrap name f = - prerr_endline (sprintf "debug_wrap: ==>> %s" name); - let res = f () in - prerr_endline (sprintf "debug_wrap: <<== %s" name); - res - +let list_tl_at ?(equality=(==)) e l = + let rec aux = + function + | [] -> raise Not_found + | hd :: tl as l when equality hd e -> l + | hd :: tl -> aux tl + in + aux l