| author | wenzelm |
| Mon, 23 Mar 2015 16:10:32 +0100 | |
| changeset 59784 | bc04a20e5a37 |
| parent 59350 | acba5d6fdb2f |
| child 62296 | b04a5ddd6121 |
| 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 |
{
|
21 |
private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
|
|
22 |
||
|
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
23 |
def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
|
|
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
24 |
|
|
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
59341
diff
changeset
|
25 |
def prover_args: List[String] = List("-P", "127.0.0.1:" + server.getLocalPort)
|
| 45028 | 26 |
|
27 |
def rendezvous(): (OutputStream, InputStream) = |
|
28 |
{
|
|
29 |
val socket = server.accept |
|
|
54340
18c621069bf8
prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;
wenzelm
parents:
54005
diff
changeset
|
30 |
socket.setTcpNoDelay(true) |
| 45028 | 31 |
(socket.getOutputStream, socket.getInputStream) |
32 |
} |
|
33 |
||
34 |
def accepted() { server.close }
|
|
35 |
} |