]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite/grafiteMarshal.ml
added ensure_path_exists to save_moo
[helm.git] / helm / ocaml / grafite / grafiteMarshal.ml
index 8b4f8858b8bf8f3b33b0b50f0670c1499d370d80..bf02e91ac575604f0934e2d93521c4d7db4045f5 100644 (file)
@@ -27,7 +27,7 @@ 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 ast_command = Cic.obj GrafiteAst.command
 type moo = ast_command list
 
 let marshal_flags = []
@@ -50,13 +50,14 @@ let rehash_cmd_uris =
       in
       let appl_pattern = aux cic_appl_pattern in
       GrafiteAst.Interpretation (loc, dsc, args, appl_pattern)
-  | GrafiteAst.Coercion (loc, term, close) ->
-      GrafiteAst.Coercion (loc, CicUtil.rehash_term term, close)
+  | GrafiteAst.Coercion (loc, uri, close) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close)
   | GrafiteAst.Notation _
   | GrafiteAst.Alias _ as cmd -> cmd
   | cmd ->
       prerr_endline "Found a command not expected in a .moo:";
-      prerr_endline (GrafiteAstPp.pp_cic_command cmd);
+      let obj_pp _ = assert false in
+      prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd);
       assert false
 
 (** .moo file format
@@ -68,6 +69,11 @@ let rehash_cmd_uris =
  *)
 
 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