src/Pure/System/system_channel.scala
author wenzelm
Thu, 06 Aug 2020 22:54:22 +0200
changeset 72104 d9a42786fbc9
parent 69572 09a6a7c04b45
child 73340 0ffcad1f6130
permissions -rw-r--r--
more thorough cleanup, e.g. before ML_Heap.save;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/system_channel.scala
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     3
59350
acba5d6fdb2f discontinued fifo channel, always use portable socket;
wenzelm
parents: 59341
diff changeset
     4
Socket-based system channel for inter-process communication.
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     5
*/
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     6
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     7
package isabelle
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     8
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     9
59350
acba5d6fdb2f discontinued fifo channel, always use portable socket;
wenzelm
parents: 59341
diff changeset
    10
import java.io.{InputStream, OutputStream}
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    11
import java.net.{ServerSocket, InetAddress}
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    12
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    13
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    14
object System_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    15
{
59350
acba5d6fdb2f discontinued fifo channel, always use portable socket;
wenzelm
parents: 59341
diff changeset
    16
  def apply(): System_Channel = new System_Channel
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    17
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    18
59350
acba5d6fdb2f discontinued fifo channel, always use portable socket;
wenzelm
parents: 59341
diff changeset
    19
class System_Channel private
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    20
{
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69124
diff changeset
    21
  private val server = new ServerSocket(0, 50, Server.localhost)
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    22
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    23
  val address: String = Server.print_address(server.getLocalPort)
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    24
  val password: String = UUID.random().toString
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    25
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    26
  override def toString: String = address
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    27
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    28
  def shutdown() { server.close }
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    29
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    30
  def rendezvous(): (OutputStream, InputStream) =
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    31
  {
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    32
    val socket = server.accept
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    33
    try {
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    34
      val out_stream = socket.getOutputStream
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    35
      val in_stream = socket.getInputStream
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    36
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    37
      if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    38
      else {
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    39
        out_stream.close
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    40
        in_stream.close
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    41
        error("Failed to connect system channel: bad password")
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    42
      }
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    43
    }
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    44
    finally { shutdown() }
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69463
diff changeset
    45
  }
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    46
}