| author | wenzelm | 
| Wed, 27 May 2020 20:02:02 +0200 | |
| changeset 71910 | f8b0271cc744 | 
| parent 69572 | 09a6a7c04b45 | 
| child 73340 | 0ffcad1f6130 | 
| permissions | -rw-r--r-- | 
| 45027 | 1 | /* Title: Pure/System/system_channel.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 59350 
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
 wenzelm parents: 
59341diff
changeset | 4 | Socket-based system channel for inter-process communication. | 
| 45027 | 5 | */ | 
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 59350 
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
 wenzelm parents: 
59341diff
changeset | 10 | import java.io.{InputStream, OutputStream}
 | 
| 45028 | 11 | import java.net.{ServerSocket, InetAddress}
 | 
| 45027 | 12 | |
| 13 | ||
| 14 | object System_Channel | |
| 15 | {
 | |
| 59350 
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
 wenzelm parents: 
59341diff
changeset | 16 | def apply(): System_Channel = new System_Channel | 
| 45027 | 17 | } | 
| 18 | ||
| 59350 
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
 wenzelm parents: 
59341diff
changeset | 19 | class System_Channel private | 
| 45028 | 20 | {
 | 
| 69463 | 21 | private val server = new ServerSocket(0, 50, Server.localhost) | 
| 45028 | 22 | |
| 69572 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
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: 
69463diff
changeset | 24 | val password: String = UUID.random().toString | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 25 | |
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 26 | override def toString: String = address | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 27 | |
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 28 |   def shutdown() { server.close }
 | 
| 45028 | 29 | |
| 30 | def rendezvous(): (OutputStream, InputStream) = | |
| 31 |   {
 | |
| 32 | val socket = server.accept | |
| 69572 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 33 |     try {
 | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 34 | val out_stream = socket.getOutputStream | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 35 | val in_stream = socket.getInputStream | 
| 45028 | 36 | |
| 69572 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
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: 
69463diff
changeset | 38 |       else {
 | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 39 | out_stream.close | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 40 | in_stream.close | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
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: 
69463diff
changeset | 42 | } | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 43 | } | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 44 |     finally { shutdown() }
 | 
| 
09a6a7c04b45
more robust system channel via options that are private to the user;
 wenzelm parents: 
69463diff
changeset | 45 | } | 
| 45028 | 46 | } |