From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 11:57:18 +0000 (+0000)
Subject: cleanup temp files on parser failure
X-Git-Tag: V_0_0_10~49
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a8397bf2db45db960899499fb59183a68778248;p=helm.git

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 e15186fde..d214d89b5 100644
--- 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
    )
 ;;