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
let baseuri_of_file file =
let uri = ref None in
let ic = open_in file in
- let istream = Stream.of_channel ic in
+ let istream = Ulexing.from_utf8_channel ic in
(try
while true do
try
else
s
-let strip_trailing_blanks =
- let rex = Pcre.regexp "\\s*$" in
- fun s -> Pcre.replace ~rex 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.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
+ aux path tl
+ in
+ aux "" components
+
+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 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
context
| _ -> []
-let get_proof_aliases status = status.aliases
-
+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 unopt = function None -> failwith "unopt: None" | Some v -> v
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
| [] -> []
| 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