+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
+ | _ -> 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_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