X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=0c4329e554350936ea863f1c2e581e13df8ca5d9;hb=aa0d60227b785da3355b31519ba11cb4fbd2c925;hp=ca8dc2446660ec11d5e424119f53be2ff4ebd6a4;hpb=35d7685022202a24dac2d0cab17796b492a8d50d;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index ca8dc2446..0c4329e55 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -23,84 +23,14 @@ * http://helm.cs.unibo.it/ *) -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 +(* $Id$ *) -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 +open Printf -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,45 +44,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 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 *) @@ -247,59 +138,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 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 list_tl_at ?(equality=(==)) e l = let rec aux = function @@ -308,10 +150,3 @@ let list_tl_at ?(equality=(==)) e l = | hd :: tl -> aux tl 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 -