* http://helm.cs.unibo.it/
*)
-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
- with Unix.Unix_error _ -> false
+(* $Id$ *)
-let is_regular fname =
- try
- (Unix.stat fname).Unix.st_kind = Unix.S_REG
- with Unix.Unix_error _ -> false
-
-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
+open Printf
-let output_file data file =
- let oc = open_out file in
- output_string oc data;
- close_out oc
+(** Functions "imported" from Http_getter_misc *)
+let normalize_dir = Http_getter_misc.normalize_dir
+let strip_suffix = Http_getter_misc.strip_suffix
let absolute_path file =
if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
else
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.error_message e)));
- aux path tl
- in
- aux "" components
-
-let strip_trailing_blanks =
- 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 () =
- DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
- ~qualifiedName:(Gdome.domString "math") ~doctype:None
-
-let empty_boxml () =
- DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns)
- ~qualifiedName:(Gdome.domString "box") ~doctype:None
-
exception History_failure
type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *)
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_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 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 list_tl_at ?(equality=(==)) e l =
let rec aux =
function
| hd :: tl -> aux tl
in
aux l
-
-let debug_wrap name f =
- prerr_endline (sprintf "debug_wrap: ==>> %s" name);
- let res = f () in
- prerr_endline (sprintf "debug_wrap: <<== %s" name);
- res
-
projects / helm.git / blobdiff