X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteMarshal.ml;h=e786d500154f4747b0128bdcf323178793278244;hb=9262517c80e17d46b9bf9931dc879ac653a633e9;hp=0c4488091503d109f639a36e53239e35c49c7662;hpb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;p=helm.git diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index 0c4488091..e786d5001 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -23,17 +23,23 @@ * http://helm.cs.unibo.it/ *) -exception Checksum_failure of string -exception Corrupt_moo of string -exception Version_mismatch of string +(* $Id$ *) type ast_command = Cic.obj GrafiteAst.command type moo = ast_command list -let marshal_flags = [] +let format_name = "grafite" + +let save_moo_to_file ~fname moo = + HMarshal.save ~fmt:format_name ~version:GrafiteAst.magic ~fname moo + +let load_moo_from_file ~fname = + let raw = HMarshal.load ~fmt:format_name ~version:GrafiteAst.magic ~fname in + (raw: moo) let rehash_cmd_uris = - let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in + let rehash_uri uri = + UriManager.uri_of_string (UriManager.string_of_uri uri) in function | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in @@ -46,44 +52,9 @@ let rehash_cmd_uris = prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd); assert false -(** .moo file format - * - an integer -- magic number -- denoting the version of the dumped data - * structure. Different magic numbers stand for incompatible data structures - * - an integer -- checksum -- denoting the hash value (computed with - * Hashtbl.hash) of the string representation of the dumped data structur - * - marshalled data: list of GrafiteAst.command - *) - -let save_moo ~fname moo = - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - ensure_path_exists fname; - let oc = open_out fname in - let marshalled = Marshal.to_string (List.rev moo) marshal_flags in - let checksum = Hashtbl.hash marshalled in - output_binary_int oc GrafiteAst.magic; - output_binary_int oc checksum; - output_string oc marshalled; - close_out oc +let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo) let load_moo ~fname = - let ic = open_in fname in - HExtlib.finally - (fun () -> close_in ic) - (fun () -> - try - let moo_magic = input_binary_int ic in - if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname); - let moo_checksum = input_binary_int ic in - let marshalled = HExtlib.input_all ic in - let checksum = Hashtbl.hash marshalled in - if checksum <> moo_checksum then raise (Checksum_failure fname); - let (moo:moo) = - Marshal.from_string marshalled 0 - in - List.map rehash_cmd_uris moo - with End_of_file -> raise (Corrupt_moo fname)) - () + let moo = load_moo_from_file ~fname in + List.map rehash_cmd_uris moo