# HG changeset patch
# User wenzelm
# Date 1663103212 -7200
# Node ID a6bdf4b889ca9f6432208fdf220efe61b7a8573b
# Parent  35a279a2d24606e3e49593df851469aa8579e26a
clarified signature;

diff -r 35a279a2d246 -r a6bdf4b889ca src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 13 23:01:42 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 23:06:52 2022 +0200
@@ -253,15 +253,8 @@
     ): Port_Forwarding = {
       if (control_path.isEmpty) error("SSH port forwarding requires multiplexing")
 
-      val port =
-        if (local_port > 0) local_port
-        else {
-          // FIXME race condition
-          val dummy = new ServerSocket(0)
-          val port = dummy.getLocalPort
-          dummy.close()
-          port
-        }
+      val port = if (local_port > 0) local_port else Isabelle_System.local_port()
+
       val string = List(local_host, port, remote_host, remote_port).mkString(":")
       run_ssh(opts = "-L " + Bash.string(string) + " -O forward").check
 
diff -r 35a279a2d246 -r a6bdf4b889ca src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 13 23:01:42 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Sep 13 23:06:52 2022 +0200
@@ -9,6 +9,7 @@
 
 import java.util.{Map => JMap, HashMap}
 import java.io.{File => JFile, IOException}
+import java.net.ServerSocket
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
   StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
@@ -349,6 +350,15 @@
   }
 
 
+  /* TCP/IP ports */
+
+  def local_port(): Int = {
+    val socket = new ServerSocket(0)
+    val port = socket.getLocalPort
+    socket.close()
+    port
+  }
+
 
   /** external processes **/