src/Pure/System/system_channel.scala
changeset 75393 87ebf5a50283
parent 73367 77ef8bef0593
child 79048 caddfe4949a8
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
     9 
     9 
    10 import java.io.{InputStream, OutputStream}
    10 import java.io.{InputStream, OutputStream}
    11 import java.net.{ServerSocket, InetAddress}
    11 import java.net.{ServerSocket, InetAddress}
    12 
    12 
    13 
    13 
    14 object System_Channel
    14 object System_Channel {
    15 {
       
    16   def apply(): System_Channel = new System_Channel
    15   def apply(): System_Channel = new System_Channel
    17 }
    16 }
    18 
    17 
    19 class System_Channel private
    18 class System_Channel private {
    20 {
       
    21   private val server = new ServerSocket(0, 50, Server.localhost)
    19   private val server = new ServerSocket(0, 50, Server.localhost)
    22 
    20 
    23   val address: String = Server.print_address(server.getLocalPort)
    21   val address: String = Server.print_address(server.getLocalPort)
    24   val password: String = UUID.random().toString
    22   val password: String = UUID.random().toString
    25 
    23 
    26   override def toString: String = address
    24   override def toString: String = address
    27 
    25 
    28   def shutdown(): Unit = server.close()
    26   def shutdown(): Unit = server.close()
    29 
    27 
    30   def rendezvous(): (OutputStream, InputStream) =
    28   def rendezvous(): (OutputStream, InputStream) = {
    31   {
       
    32     val socket = server.accept
    29     val socket = server.accept
    33     try {
    30     try {
    34       val out_stream = socket.getOutputStream
    31       val out_stream = socket.getOutputStream
    35       val in_stream = socket.getInputStream
    32       val in_stream = socket.getInputStream
    36 
    33