-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
-
-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
-
-let output_file data file =
- let oc = open_out file in
- output_string oc data;
- close_out oc