--- 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
--- 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 **/