more robust management of resources, using Thread_Attributes.uninterruptible;

--- a/src/Pure/ML/ml_compiler0.ML	Tue Sep 26 13:37:08 2023 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Tue Sep 26 14:29:55 2023 +0200
@@ -117,11 +117,12 @@
 
 end;
 
-fun ML_file context {verbose, debug} file =
+fun ML_file context {verbose, debug} file = Thread_Attributes.uninterruptible (fn run => fn () =>
   let
     val instream = TextIO.openIn file;
-    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in ML context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+    val result = Exn.capture (run TextIO.inputAll) instream;
+    val _ = TextIO.closeIn instream;
+  in ML context {line = 1, file = file, verbose = verbose, debug = debug} (Exn.release result) end) ();
 
 fun ML_file_operations (f: bool option -> string -> unit) =
   {ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)};

--- a/src/Pure/System/isabelle_system.ML	Tue Sep 26 13:37:08 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue Sep 26 14:29:55 2023 +0200
@@ -149,9 +149,13 @@
 
 fun rm_tree path = scala_function "rm_tree" [path];
 
-fun with_tmp_dir name f =
-  let val path = create_tmp_path name ""
-  in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
+fun with_tmp_dir name f = Thread_Attributes.uninterruptible (fn run => fn () =>
+  let
+    val path = create_tmp_path name "";
+    val _ = make_directory path;
+    val result = Exn.capture (run f) path;
+    val _ = try rm_tree path;
+  in Exn.release result end) ();
 
 
 (* download file *)