- added integrity checks on .moo files

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 0bd5acb9576ee33bf61e95764b5228690f5d448f..b065040523bc2d46d3fa2b4f3db89d91a9611ca9 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -634,7 +634,7 @@ let generate_projections uri fields status =
   ) status projections
 
 (* to avoid a long list of recursive functions *)
-let eval_from_dump_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
  
 let disambiguate_obj status obj =
   let uri =
@@ -712,7 +712,7 @@ let eval_command opts status cmd =
      let status = ref status in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
-     !eval_from_dump_ref status moopath (fun _ _ -> ());
+     !eval_from_moo_ref status moopath (fun _ _ -> ());
      !status
   | GrafiteAst.Set (loc, name, value) -> 
       let value = 
@@ -884,18 +884,16 @@ let eval_ast
   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_dump ?do_heavy_checks ?include_paths ?clean_baseuri status fname
+let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname
   cb
 =
-  let ic = open_in fname in
-  let moo = Marshal.from_channel ic in
-  close_in ic;
+  let moo = MatitaMoo.load_moo fname in
   List.iter 
     (fun ast -> 
       let ast =
         GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
           GrafiteAst.Command (DisambiguateTypes.dummy_floc,
-            (GrafiteAst.reash_uris ast)))
+            (GrafiteAst.reash_cmd_uris ast)))
       in
       cb !status ast;
       status :=
@@ -915,7 +913,7 @@ let eval_from_stream
   with End_of_file -> ()
 
 (* to avoid a long list of recursive functions *)
-let _ = eval_from_dump_ref := eval_from_dump
+let _ = eval_from_moo_ref := eval_from_moo
   
 let eval_from_stream_greedy 
   ?do_heavy_checks ?include_paths ?clean_baseuri status str cb