open Printf
open MatitaTypes
-let strip_trailing_slash =
- let rex = Pcre.regexp "/$" in
- fun s -> Pcre.replace ~rex s
+(** 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
| piece::tl ->
let path = where ^ "/" ^ piece in
(try
- Unix.mkdir path 755
+ Unix.mkdir path 0o755
with
| Unix.Unix_error (Unix.EEXIST,_,_) -> ()
| Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
in
aux "" components
-let strip_trailing_blanks =
- let rex = Pcre.regexp "\\s*$" in
- fun s -> Pcre.replace ~rex s
+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 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
- let dir = "mkdir -p " ^ d in
- (match Unix.system dir with
- | Unix.WEXITED 0 -> ()
- | 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
| Incomplete_proof s -> s
path ^ ".moo"
let obj_file_of_script f =
- let baseuri = baseuri_of_file f in
- obj_file_of_baseuri baseuri
+ 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
| [] -> []