| author | wenzelm | 
| Sat, 08 Oct 2016 10:59:38 +0200 | |
| changeset 64098 | 099518e8af2c | 
| parent 62306 | 5c0a5c30cda8 | 
| 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: 
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 | {
 | 
| 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: 
54005diff
changeset | 29 | socket.setTcpNoDelay(true) | 
| 45028 | 30 | (socket.getOutputStream, socket.getInputStream) | 
| 31 | } | |
| 32 | ||
| 33 |   def accepted() { server.close }
 | |
| 34 | } |