X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=e86e4b9a051e33ecfc81ab671b25cc7bd4359c48;hb=86af949158e013178557c7fec7662ac06fae753c;hp=99fea1a32cec09944963043c058fdeda576bd9d0;hpb=2a953f2a05308ee417f63dceb29e027c527d4e17;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 99fea1a32..e86e4b9a0 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -26,31 +26,82 @@ open Printf open MatitaTypes -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 +(** 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 output_file data file = - let oc = open_out file in - output_string oc data; - close_out oc +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 @@ -64,14 +115,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 strip_trailing_slash = - let rex = Pcre.regexp "/$" in - fun s -> Pcre.replace ~rex s - let empty_mathml () = DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) ~qualifiedName:(Gdome.domString "math") ~doctype:None @@ -174,25 +217,6 @@ 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 @@ -212,16 +236,30 @@ let get_proof_context status = context | _ -> [] -let get_proof_aliases status = status.aliases - +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$" -let obj_file_of_script f = Pcre.replace ~rex:end_ma_RE ~templ:".moo" f + +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 | [] -> [] @@ -229,9 +267,12 @@ let rec list_uniq = function | 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