# HG changeset patch
# User wenzelm
# Date 1663354496 -7200
# Node ID b847a9983784b6826bfe477c4849cafae7743076
# Parent  d6bd84eb94a39bdb8064310edb0f65b7a11e3284
tuned signature;

diff -r d6bd84eb94a3 -r b847a9983784 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Sep 16 16:34:45 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Sep 16 20:54:56 2022 +0200
@@ -282,8 +282,12 @@
     file
   }
 
-  def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = {
-    val file = tmp_file(name, ext)
+  def with_tmp_file[A](
+    name: String,
+    ext: String = "",
+    base_dir: JFile = isabelle_tmp_prefix()
+  )(body: Path => A): A = {
+    val file = tmp_file(name, ext, base_dir = base_dir)
     try { body(File.path(file)) } finally { file.delete }
   }
 
@@ -327,8 +331,11 @@
     dir
   }
 
-  def with_tmp_dir[A](name: String)(body: Path => A): A = {
-    val dir = tmp_dir(name)
+  def with_tmp_dir[A](
+    name: String,
+    base_dir: JFile = isabelle_tmp_prefix()
+  )(body: Path => A): A = {
+    val dir = tmp_dir(name, base_dir = base_dir)
     try { body(File.path(dir)) } finally { rm_tree(dir) }
   }