author | wenzelm |
Fri, 24 Nov 2023 14:11:01 +0100 | |
changeset 79048 | caddfe4949a8 |
parent 75393 | 87ebf5a50283 |
child 79049 | 10b6add456d0 |
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 |
||
75393 | 14 |
object System_Channel { |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
59341
diff
changeset
|
15 |
def apply(): System_Channel = new System_Channel |
45027 | 16 |
} |
17 |
||
75393 | 18 |
class System_Channel private { |
69463 | 19 |
private val server = new ServerSocket(0, 50, Server.localhost) |
45028 | 20 |
|
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
21 |
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
|
22 |
val password: String = UUID.random().toString |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
23 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
24 |
override def toString: String = address |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
25 |
|
73367 | 26 |
def shutdown(): Unit = server.close() |
45028 | 27 |
|
75393 | 28 |
def rendezvous(): (OutputStream, InputStream) = { |
45028 | 29 |
val socket = server.accept |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
30 |
try { |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
31 |
val out_stream = socket.getOutputStream |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
32 |
val in_stream = socket.getInputStream |
45028 | 33 |
|
79048 | 34 |
Byte_Message.read_line(in_stream) match { |
35 |
case Some(bs) if bs.text == password => (out_stream, in_stream) |
|
36 |
case _ => |
|
37 |
out_stream.close() |
|
38 |
in_stream.close() |
|
39 |
error("Failed to connect system channel: bad password") |
|
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
40 |
} |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
41 |
} |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
42 |
finally { shutdown() } |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
43 |
} |
45028 | 44 |
} |