| author | desharna |
| Fri, 12 Nov 2021 08:51:45 +0100 | |
| changeset 74762 | 8362a5b2c2dd |
| parent 73367 | 77ef8bef0593 |
| child 75393 | 87ebf5a50283 |
| 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:
59341
diff
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:
59341
diff
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:
59341
diff
changeset
|
16 |
def apply(): System_Channel = new System_Channel |
| 45027 | 17 |
} |
18 |
||
|
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
59341
diff
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:
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 |
|
| 73367 | 28 |
def shutdown(): Unit = 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:
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 | 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 {
|
| 73367 | 39 |
out_stream.close() |
40 |
in_stream.close() |
|
|
69572
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 | 46 |
} |