# HG changeset patch
# User wenzelm
# Date 1695733487 -7200
# Node ID 3636dc23aa0eb082987b92781ed4c397f5a89a5c
# Parent  1f5f712fc2fcd3b4dde999b08f30c66ae7d1254d
more robust management of resources, using Thread_Attributes.uninterruptible;

diff -r 1f5f712fc2fc -r 3636dc23aa0e src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Tue Sep 26 15:03:02 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue Sep 26 15:04:47 2023 +0200
@@ -140,9 +140,12 @@
       raise Fail ("Temporary file already exists: " ^ Path.print path);
   in path end;
 
-fun with_tmp_file name ext f =
-  let val path = create_tmp_path name ext
-  in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
+fun with_tmp_file name ext = Thread_Attributes.uninterruptible (fn run => fn f =>
+  let
+    val path = create_tmp_path name ext;
+    val result = Exn.capture (run f) path;
+    val _ = try File.rm path;
+  in Exn.release result end);
 
 
 (* tmp dirs *)