--- a/src/Pure/General/file.ML Wed Dec 19 21:37:48 2018 +0100
+++ b/src/Pure/General/file.ML Wed Dec 19 21:38:57 2018 +0100
@@ -92,9 +92,12 @@
local
-fun with_file open_file close_file f path =
- let val file = open_file path
- in Exn.release (Exn.capture f file before close_file file) end;
+fun with_file open_file close_file f =
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+ let
+ val file = open_file path;
+ val result = Exn.capture (restore_attributes f) file;
+ in close_file file; Exn.release result end);
in