X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=8f97b25a9384b9f77f8ec1b7f0aab49893f7526d;hb=9f02c52b23c8f56a3deaab6f5eae29ca2c3acb9f;hp=0bb2ea7e0ec2101e5726838d6cad4cdc12a05a76;hpb=6187b40af194fb960d91653682a0eb2096f20f3b;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 0bb2ea7e0..8f97b25a9 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 @@ -24,18 +24,88 @@ *) open Printf +open MatitaTypes -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 +(** Functions "imported" from Http_getter_misc *) -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 +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_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 + let is_proof_script fname = true (** TODO Zack *) let is_proof_object fname = true (** TODO Zack *) @@ -45,16 +115,13 @@ let append_phrase_sep s = else s -let strip_trailing_blanks = - let rex = Pcre.regexp "\\s*$" in - fun s -> Pcre.replace ~rex s +let empty_mathml () = + DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None -let empty_mathml = - let doc = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) - ~qualifiedName:(Gdome.domString "math") ~doctype:None - in - doc#get_documentElement +let empty_boxml () = + DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) + ~qualifiedName:(Gdome.domString "box") ~doctype:None exception History_failure @@ -67,17 +134,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; @@ -103,9 +183,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; @@ -117,12 +197,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'; @@ -130,19 +213,60 @@ class ['a] browser_history ?memento size init = method save = (Array.copy data, hd, tl, cur) end -let dbd_instance = - let dbd = lazy ( - Mysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") - ()) - in - fun () -> Lazy.force dbd - let singleton f = let instance = lazy (f ()) in fun () -> Lazy.force instance -let mkdirs = List.iter (fun d -> ignore (Unix.system ("mkdir -p " ^ d))) +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 qualify status name = get_string_option status "baseuri" ^ "/" ^ name + +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 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