ocaml 3.09 transition

[helm.git] / helm / matita / matitaMoo.ml

diff --git a/helm/matita/matitaMoo.ml b/helm/matita/matitaMoo.ml
index ea5c748bdff6e1647c63738b3e61659c3de1af93..bdea339b7c0ab94a0227f68e1d0ad222acdb2f1d 100644 (file)
--- a/helm/matita/matitaMoo.ml
+++ b/helm/matita/matitaMoo.ml
@@ -34,16 +34,19 @@ let marshal_flags = []
  *   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 list of GrafiteAst.command
+ * - marshalled pair: first component is a list of GrafiteAst.command (real moo
+ *   content), second component is a list of GrafiteAst.metadata
  *)
 
-let save_moo ~fname moo =
+let save_moo ~fname (moo, metadata) =
  let oc = open_out fname in
- let marshalled_moo = Marshal.to_string (List.rev moo) marshal_flags in
- let checksum = Hashtbl.hash marshalled_moo in
+ let marshalled = 
+   Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags 
+ in
+ let checksum = Hashtbl.hash marshalled in
  output_binary_int oc GrafiteAst.magic;
  output_binary_int oc checksum;
- output_string oc marshalled_moo;
+ output_string oc marshalled;
  close_out oc
 
 let load_moo ~fname =
@@ -55,11 +58,11 @@ let load_moo ~fname =
         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_moo = HExtlib.input_all ic in
-        let checksum = Hashtbl.hash marshalled_moo 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: MatitaTypes.ast_command list) =
-          Marshal.from_string marshalled_moo 0
+        let (moo: MatitaTypes.moo) =
+          Marshal.from_string marshalled 0
         in
         moo
       with End_of_file -> raise (Corrupt_moo fname))