--- a/src/Pure/System/system_channel.scala Sun Jan 11 13:44:25 2015 +0100
+++ b/src/Pure/System/system_channel.scala Sun Jan 11 20:40:14 2015 +0100
@@ -1,87 +1,28 @@
/* Title: Pure/System/system_channel.scala
Author: Makarius
-Portable system channel for inter-process communication, based on
-named pipes or sockets.
+Socket-based system channel for inter-process communication.
*/
package isabelle
-import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
- FileOutputStream, IOException}
+import java.io.{InputStream, OutputStream}
import java.net.{ServerSocket, InetAddress}
object System_Channel
{
- def apply(): System_Channel = new Socket_Channel
- // FIXME if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
-}
-
-abstract class System_Channel
-{
- def params: List[String]
- def prover_args: List[String]
- def rendezvous(): (OutputStream, InputStream)
- def accepted(): Unit
-}
-
-
-/** named pipes **/
-
-private object Fifo_Channel
-{
- private val next_fifo = Counter.make()
+ def apply(): System_Channel = new System_Channel
}
-private class Fifo_Channel extends System_Channel
-{
- require(!Platform.is_windows)
-
- private def mk_fifo(): String =
- {
- val i = Fifo_Channel.next_fifo()
- val script =
- "FIFO=\"${TMPDIR:-/tmp}/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
- "echo -n \"$FIFO\"\n" +
- "mkfifo -m 600 \"$FIFO\"\n"
- val result = Isabelle_System.bash(script)
- if (result.rc == 0) result.out else error(result.err)
- }
-
- private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete
-
- private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo)
- private def fifo_output_stream(fifo: String): OutputStream = new FileOutputStream(fifo)
-
- private val fifo1 = mk_fifo()
- private val fifo2 = mk_fifo()
-
- def params: List[String] = List(fifo1, fifo2)
-
- val prover_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
-
- def rendezvous(): (OutputStream, InputStream) =
- {
- val output_stream = fifo_output_stream(fifo1)
- val input_stream = fifo_input_stream(fifo2)
- (output_stream, input_stream)
- }
-
- def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
-}
-
-
-/** sockets **/
-
-private class Socket_Channel extends System_Channel
+class System_Channel private
{
private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
- def prover_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
+ def prover_args: List[String] = List("-P", "127.0.0.1:" + server.getLocalPort)
def rendezvous(): (OutputStream, InputStream) =
{