X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=3ed1f001c2d17f5c2b185362b71f1fd0f0e443a8;hb=b8c0504c5602b08443cec0782670bd4a699cbc23;hp=58fa388091e7c165ff76783141c82e6d55efd798;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 58fa38809..3ed1f001c 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -26,6 +26,58 @@ 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 @@ -44,6 +96,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 *) @@ -57,12 +118,24 @@ 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 () = - 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 @@ -76,17 +149,30 @@ class type ['a] history = method previous : 'a method load: 'a memento -> unit method save: 'a memento + method is_begin: bool + method is_end: bool end +class basic_history (head, tail, cur) = + object + val mutable hd = head (* insertion point *) + val mutable tl = tail (* oldest inserted item *) + val mutable cur = cur (* current item for the history *) + + method is_begin = cur <= tl + method is_end = cur >= hd + end + + class shell_history size = let size = size + 1 in let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in let incr x = (x + 1) mod size in object (self) val data = Array.create size "" - val mutable hd = 0 (* insertion point *) - val mutable tl = -1 (* oldest inserted item *) - val mutable cur = -1 (* current item for the history *) + + inherit basic_history (0, -1 , -1) + method add s = data.(hd) <- s; if tl = -1 then tl <- hd; @@ -112,9 +198,9 @@ class ['a] browser_history ?memento size init = object (self) initializer match memento with Some m -> self#load m | _ -> () val data = Array.create size init - val mutable hd = 0 - val mutable tl = 0 - val mutable cur = 0 + + inherit basic_history (0, 0, 0) + method previous = if cur = tl then raise History_failure; cur <- cur - 1; @@ -126,12 +212,15 @@ class ['a] browser_history ?memento size init = if cur = size then cur <- 0; data.(cur) method add (e:'a) = - cur <- cur + 1; - if cur = size then cur <- 0; - if cur = tl then tl <- tl + 1; - if tl = size then tl <- 0; - hd <- cur; - data.(cur) <- e + if e <> data.(cur) then + begin + cur <- cur + 1; + if cur = size then cur <- 0; + if cur = tl then tl <- tl + 1; + if tl = size then tl <- 0; + hd <- cur; + data.(cur) <- e + end method load (data', hd', tl', cur') = assert (Array.length data = Array.length data'); hd <- hd'; tl <- tl'; cur <- cur'; @@ -146,10 +235,21 @@ let singleton f = let mkdir d = let errmsg = sprintf "Unable to create directory \"%s\"" d in try - (match Unix.system ("mkdir -p " ^ d) with + let dir = "mkdir -p " ^ d in + (match Unix.system dir with | Unix.WEXITED 0 -> () - | _ -> failwith errmsg) - with Unix.Unix_error _ -> failwith errmsg + | 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 @@ -169,8 +269,37 @@ let get_proof_context status = 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 +