X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=e3aadd5b5a616d143c17dd22ab71d25f7ac06626;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=f332fcbd1e684bce9dbbcca5d3d546bfdc033dbb;hpb=1d431843f49b3658593c8cc918b53a43479a6486;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index f332fcbd1..e3aadd5b5 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,8 +23,70 @@ * http://helm.cs.unibo.it/ *) -let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR -let is_regular fname = (Unix.stat fname).Unix.st_kind = Unix.S_REG +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 @@ -34,6 +96,223 @@ 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 *) +let append_phrase_sep s = + if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then + s ^ BuildTimeConf.phrase_sep + 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 *) + +class type ['a] history = + object + method add : 'a -> unit + method next : 'a + 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 "" + + inherit basic_history (0, -1 , -1) + + method add s = + data.(hd) <- s; + if tl = -1 then tl <- hd; + hd <- incr hd; + if hd = tl then tl <- incr tl; + cur <- hd + method previous = + if cur = tl then raise History_failure; + cur <- decr cur; + data.(cur) + method next = + if cur = hd then raise History_failure; + cur <- incr cur; + if cur = hd then "" else data.(cur) + method load (data', hd', tl', cur') = + assert (Array.length data = Array.length data'); + hd <- hd'; tl <- tl'; cur <- cur'; + Array.blit data' 0 data 0 (Array.length data') + method save = (Array.copy data, hd, tl, cur) + end + +class ['a] browser_history ?memento size init = + object (self) + initializer match memento with Some m -> self#load m | _ -> () + val data = Array.create size init + + inherit basic_history (0, 0, 0) + + method previous = + if cur = tl then raise History_failure; + cur <- cur - 1; + if cur = ~-1 then cur <- size - 1; + data.(cur) + method next = + if cur = hd then raise History_failure; + cur <- cur + 1; + if cur = size then cur <- 0; + data.(cur) + method add (e:'a) = + 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'; + Array.blit data' 0 data 0 (Array.length data') + method save = (Array.copy data, hd, tl, cur) + end + +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 = + 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 +