From 2a8397bf2db45db960899499fb59183a68778248 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Oct 2004 11:57:18 +0000 Subject: [PATCH] cleanup temp files on parser failure --- .../cic_proof_checking/cicEnvironment.ml | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) 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 ) ;; -- 2.39.2