| author | wenzelm | 
| Sun, 14 Feb 2016 13:11:19 +0100 | |
| changeset 62306 | 5c0a5c30cda8 | 
| parent 62299 | 9e95a4afb8c3 | 
| child 66346 | 30663525e057 | 
| 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  | 
||
| 62306 | 23  | 
val server_name: String = "127.0.0.1:" + server.getLocalPort  | 
24  | 
override def toString: String = server_name  | 
|
| 45028 | 25  | 
|
26  | 
def rendezvous(): (OutputStream, InputStream) =  | 
|
27  | 
  {
 | 
|
28  | 
val socket = server.accept  | 
|
| 
54340
 
18c621069bf8
prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;
 
wenzelm 
parents: 
54005 
diff
changeset
 | 
29  | 
socket.setTcpNoDelay(true)  | 
| 45028 | 30  | 
(socket.getOutputStream, socket.getInputStream)  | 
31  | 
}  | 
|
32  | 
||
33  | 
  def accepted() { server.close }
 | 
|
34  | 
}  |