From 1f33314961ad955e6ed5314a499089f3138dfe69 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Apr 2020 13:22:11 +0200
Subject: Close files in fetch_delayed

Close #12192

Also removed transforming arbitrary exceptions into Faulty to make it
easier to reason about exception flow
---
 vernac/library.ml | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/vernac/library.ml b/vernac/library.ml
index 35b2a18871..5fddaa759b 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -57,14 +57,18 @@ let in_delayed f ch ~segment =
 
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
-  try
-    let ch = open_in_bin f in
-    let () = LargeFile.seek_in ch pos in
-    let obj = System.marshal_in f ch in
-    let digest' = Digest.input ch in
-    if not (String.equal digest digest') then raise (Faulty f);
-    obj
-  with e when CErrors.noncritical e -> raise (Faulty f)
+  let ch = open_in_bin f in
+  let obj, digest' =
+    try
+      let () = LargeFile.seek_in ch pos in
+      let obj = System.marshal_in f ch in
+      let digest' = Digest.input ch in
+      obj, digest'
+    with e -> close_in ch; raise e
+  in
+  close_in ch;
+  if not (String.equal digest digest') then raise (Faulty f);
+  obj
 
 end
 
@@ -200,7 +204,7 @@ let access_table what tables dp i =
         with Faulty f ->
           user_err ~hdr:"Library.access_table"
             (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
-             str ") is inaccessible or corrupted,\ncannot load some " ++
+             str ") is corrupted,\ncannot load some " ++
              str what ++ str " in it.\n")
       in
       tables := DPmap.add dp (Fetched t) !tables;
-- 
cgit v1.2.3