X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=56cb4a29535f1734b5db12cc3c09410971be69ed;hb=5b32b7905bc78c11e353efd68137b8eb7b6ac73b;hp=a35a57ed644943103e5c5a9e22806abc28445df9;hpb=ccca8f161bcbe57b58e651656a4a825c5227abf2;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index a35a57ed6..56cb4a295 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -26,6 +26,60 @@ 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 fname = try (Unix.stat fname).Unix.st_kind = Unix.S_DIR @@ -44,6 +98,15 @@ let input_file fname = 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 absolute_path file = + if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file + let is_proof_script fname = true (** TODO Zack *) let is_proof_object fname = true (** TODO Zack *) @@ -53,16 +116,46 @@ let append_phrase_sep s = else s -let strip_trailing_blanks = - let rex = Pcre.regexp "\\s*$" in - fun s -> Pcre.replace ~rex 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.mkdir " ^ path ^ " 0o755 :" ^ (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 () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) + DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) ~qualifiedName:(Gdome.domString "math") ~doctype:None let empty_boxml () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) + DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) ~qualifiedName:(Gdome.domString "box") ~doctype:None exception History_failure @@ -159,14 +252,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 - (match Unix.system ("mkdir -p " ^ d) with - | Unix.WEXITED 0 -> () - | _ -> failwith errmsg) - with Unix.Unix_error _ -> failwith errmsg - let get_proof_status status = match status.proof_status with | Incomplete_proof s -> s @@ -186,11 +271,51 @@ 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_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 + | [] -> raise Not_found + | hd :: tl as l when equality hd 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 +