cleanup temp files on parser failure

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 8014a19404d99da98716962b039b203ef559e97d..d214d89b5cf0be3157fc252e2199eec5da3968d5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -38,6 +38,7 @@
 let cleanup_tmp = true;;
 
 let trust_obj = function uri -> true;;
+(*let trust_obj = function uri -> false;;*)
 
 type type_checked_obj =
    CheckedObj of Cic.obj     (* cooked obj *)
@@ -317,14 +318,25 @@ let find_or_add_unchecked_to_cache uri =
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
-      let obj = CicParser.obj_of_xml filename bodyfilename in
+     let cleanup () =
        if cleanup_tmp then
         begin
-         Unix.unlink filename ;
+         if Sys.file_exists filename then Unix.unlink filename ;
          match bodyfilename with
-            Some f -> Unix.unlink f
+            Some f -> if Sys.file_exists f then Unix.unlink f
           | None -> ()
         end ;
+      in
+      CicUniv.directly_to_env_begin ();
+      let obj =
+        try
+          CicParser.obj_of_xml filename bodyfilename
+        with exn ->
+          cleanup ();
+          raise exn
+      in
+      CicUniv.directly_to_env_end ();
+      cleanup ();
        obj
    )
 ;;
@@ -405,3 +417,11 @@ let in_cache uri =
   ignore (Cache.find_cooked uri);true
  with Not_found -> false
 ;;
+
+let add_type_checked_term uri obj =
+  match obj with 
+  Cic.Constant (s,(Some bo),ty,ul) ->
+    Cache.add_cooked ~key:uri obj
+  | _ -> assert false 
+  Cache.add_cooked 
+;;