clarified signature;
authorwenzelm
Tue, 13 Sep 2022 23:01:42 +0200
changeset 76144 35a279a2d246
parent 76142 e8d4013c49d1
child 76145 a6bdf4b889ca
clarified signature;
src/Pure/General/ssh.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 13 22:36:41 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 23:01:42 2022 +0200
@@ -82,11 +82,7 @@
     multiplex: Boolean = !Platform.is_windows
   ): Session = {
     val (control_master, control_path) =
-      if (multiplex) {
-        val file = Isabelle_System.tmp_file("ssh_socket")
-        file.delete()
-        (true, file.getPath)
-      }
+      if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", initialized = false).getPath)
       else (false, "")
 
     new Session(options, host, port, user, control_master, control_path)
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 13 22:36:41 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Sep 13 23:01:42 2022 +0200
@@ -269,10 +269,15 @@
     File.platform_file(path)
   }
 
-  def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = {
+  def tmp_file(
+    name: String,
+    ext: String = "",
+    base_dir: JFile = isabelle_tmp_prefix(),
+    initialized: Boolean = true
+  ): JFile = {
     val suffix = if (ext == "") "" else "." + ext
     val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
-    file.deleteOnExit()
+    if (initialized) file.deleteOnExit() else file.delete()
     file
   }