cleanup temp files on parser failure

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index e15186fdecdb489f437d50c91bbad63b3e54e00c..d214d89b5cf0be3157fc252e2199eec5da3968d5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -318,16 +318,25 @@ let find_or_add_unchecked_to_cache uri =
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
-      CicUniv.directly_to_env_begin ();
-      let obj = CicParser.obj_of_xml filename bodyfilename in
-      CicUniv.directly_to_env_end ();
+     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
    )
 ;;