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
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 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
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';
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
| _ -> []
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
+