| author | wenzelm | 
| Wed, 17 Jun 2015 22:30:22 +0200 | |
| changeset 60511 | 5e67a223a141 | 
| 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: 
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 | ||
| 54005 
132640f4c453
tuned signature -- facilitate experimentation with other processes;
 wenzelm parents: 
52537diff
changeset | 23 |   def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
 | 
| 
132640f4c453
tuned signature -- facilitate experimentation with other processes;
 wenzelm parents: 
52537diff
changeset | 24 | |
| 59350 
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
 wenzelm parents: 
59341diff
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: 
54005diff
changeset | 30 | socket.setTcpNoDelay(true) | 
| 45028 | 31 | (socket.getOutputStream, socket.getInputStream) | 
| 32 | } | |
| 33 | ||
| 34 |   def accepted() { server.close }
 | |
| 35 | } |