X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMoo.ml;h=bdea339b7c0ab94a0227f68e1d0ad222acdb2f1d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ea5c748bdff6e1647c63738b3e61659c3de1af93;hpb=b2f2e47efe1e01df81cb7659c30eeb76f1f830da;p=helm.git

diff --git a/helm/matita/matitaMoo.ml b/helm/matita/matitaMoo.ml
index ea5c748bd..bdea339b7 100644
--- 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))