X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteMarshal.ml;h=0c4488091503d109f639a36e53239e35c49c7662;hb=18c6848695fbfa97508e0981f6875a6459429a58;hp=dd9febedbc66fe9f384395fe47229a972b6eb905;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index dd9febedb..0c4488091 100644
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -27,25 +27,41 @@ exception Checksum_failure of string
 exception Corrupt_moo of string
 exception Version_mismatch of string
 
-type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
+type ast_command = Cic.obj GrafiteAst.command
+type moo = ast_command list
 
 let marshal_flags = []
 
+let rehash_cmd_uris =
+  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
+      GrafiteAst.Default (loc, name, uris)
+  | GrafiteAst.Coercion (loc, uri, close) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close)
+  | cmd ->
+      prerr_endline "Found a command not expected in a .moo:";
+      let obj_pp _ = assert false in
+      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 pair: first component is a list of GrafiteAst.command (real moo
- *   content), second component is a list of GrafiteAst.metadata
+ * - marshalled data: list of GrafiteAst.command
  *)
 
-let save_moo ~fname (moo, metadata) =
- let oc = open_out fname in
- let marshalled = 
-   Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags 
+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;
@@ -67,7 +83,7 @@ let load_moo ~fname =
         let (moo:moo) =
           Marshal.from_string marshalled 0
         in
-        moo
+        List.map rehash_cmd_uris moo
       with End_of_file -> raise (Corrupt_moo fname))
     ()