more abstract wrapping of fifos as System_Channel;

--- a/src/Pure/System/isabelle_process.scala	Wed Sep 21 17:50:25 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed Sep 21 20:35:50 2011 +0200
@@ -96,7 +96,7 @@
 
   private def put_result(kind: String, props: Properties.T, body: XML.Body)
   {
-    if (kind == Markup.INIT) rm_fifos()
+    if (kind == Markup.INIT) system_channel.accepted()
     if (kind == Markup.RAW)
       receiver(new Result(XML.Elem(Markup(kind, props), body)))
     else {
@@ -131,18 +131,16 @@
 
   /** process manager **/
 
-  private val in_fifo = Isabelle_System.mk_fifo()
-  private val out_fifo = Isabelle_System.mk_fifo()
-  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
+  private val system_channel = System_Channel()
 
   private val process =
     try {
       val cmdline =
-        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
-          in_fifo + ":" + out_fifo) ++ args
+        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
+          (system_channel.isabelle_args ::: args.toList)
       new Isabelle_System.Managed_Process(true, cmdline: _*)
     }
-    catch { case e: IOException => rm_fifos(); throw(e) }
+    catch { case e: IOException => system_channel.accepted(); throw(e) }
 
   val process_result =
     Simple_Thread.future("process_result") { process.join }
@@ -182,9 +180,7 @@
       process_result.join
     }
     else {
-      // rendezvous
-      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
-      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
+      val (command_stream, message_stream) = system_channel.rendezvous()
 
       standard_input = stdin_actor()
       val stdout = stdout_actor()
@@ -197,7 +193,7 @@
       system_result("process_manager terminated")
       put_result(Markup.EXIT, "Return code: " + rc.toString)
     }
-    rm_fifos()
+    system_channel.accepted()
   }
 
 

--- a/src/Pure/System/isabelle_system.scala	Wed Sep 21 17:50:25 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Sep 21 20:35:50 2011 +0200
@@ -10,8 +10,8 @@
 import java.lang.System
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
-  BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException}
+import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
+  BufferedWriter, OutputStreamWriter, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -108,7 +108,7 @@
   def standard_path(path: Path): String = path.expand.implode
 
   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
-  def platform_file(path: Path) = new File(platform_path(path))
+  def platform_file(path: Path): File = new File(platform_path(path))
 
   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
 
@@ -266,54 +266,6 @@
   }
 
 
-  /* named pipes */
-
-  private val next_fifo = new Counter
-
-  def mk_fifo(): String =
-  {
-    val i = next_fifo()
-    val script =
-      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
-      "echo -n \"$FIFO\"\n" +
-      "mkfifo -m 600 \"$FIFO\"\n"
-    val (out, err, rc) = bash(script)
-    if (rc == 0) out else error(err.trim)
-  }
-
-  def rm_fifo(fifo: String): Boolean =
-    (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
-
-  def fifo_input_stream(fifo: String): InputStream =
-  {
-    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
-      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
-      proc.getOutputStream.close
-      proc.getErrorStream.close
-      proc.getInputStream
-    }
-    else new FileInputStream(fifo)
-  }
-
-  def fifo_output_stream(fifo: String): OutputStream =
-  {
-    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
-      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
-      proc.getInputStream.close
-      proc.getErrorStream.close
-      val out = proc.getOutputStream
-      new OutputStream {
-        override def close() { out.close(); proc.waitFor() }
-        override def flush() { out.flush() }
-        override def write(b: Array[Byte]) { out.write(b) }
-        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
-        override def write(b: Int) { out.write(b) }
-      }
-    }
-    else new FileOutputStream(fifo)
-  }
-
-
 
   /** Isabelle resources **/
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/system_channel.scala	Wed Sep 21 20:35:50 2011 +0200
@@ -0,0 +1,100 @@
+/*  Title:      Pure/System/system_channel.scala
+    Author:     Makarius
+
+Portable system channel for inter-process communication.
+*/
+
+package isabelle
+
+
+import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
+
+
+object System_Channel
+{
+  def apply(): System_Channel = new Fifo_Channel
+}
+
+abstract class System_Channel
+{
+  def isabelle_args: List[String]
+  def rendezvous(): (OutputStream, InputStream)
+  def accepted(): Unit
+}
+
+
+object Fifo_Channel
+{
+  private val next_fifo = new Counter
+}
+
+class Fifo_Channel extends System_Channel
+{
+  /* operations on named pipes */
+
+  private def mk_fifo(): String =
+  {
+    val i = Fifo_Channel.next_fifo()
+    val script =
+      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
+      "echo -n \"$FIFO\"\n" +
+      "mkfifo -m 600 \"$FIFO\"\n"
+    val (out, err, rc) = Isabelle_System.bash(script)
+    if (rc == 0) out else error(err.trim)
+  }
+
+  private def rm_fifo(fifo: String): Boolean =
+    Isabelle_System.platform_file(
+      Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
+
+  private def fifo_input_stream(fifo: String): InputStream =
+  {
+    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
+      val proc =
+        Isabelle_System.execute(false,
+          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
+      proc.getOutputStream.close
+      proc.getErrorStream.close
+      proc.getInputStream
+    }
+    else new FileInputStream(fifo)
+  }
+
+  private def fifo_output_stream(fifo: String): OutputStream =
+  {
+    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
+      val proc =
+        Isabelle_System.execute(false,
+          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
+      proc.getInputStream.close
+      proc.getErrorStream.close
+      val out = proc.getOutputStream
+      new OutputStream {
+        override def close() { out.close(); proc.waitFor() }
+        override def flush() { out.flush() }
+        override def write(b: Array[Byte]) { out.write(b) }
+        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
+        override def write(b: Int) { out.write(b) }
+      }
+    }
+    else new FileOutputStream(fifo)
+  }
+
+
+  /* initialization */
+
+  private val fifo1 = mk_fifo()
+  private val fifo2 = mk_fifo()
+
+  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
+
+  def rendezvous(): (OutputStream, InputStream) =
+  {
+    /*rendezvous*/
+    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) }
+}

--- a/src/Pure/build-jars	Wed Sep 21 17:50:25 2011 +0200
+++ b/src/Pure/build-jars	Wed Sep 21 20:35:50 2011 +0200
@@ -49,6 +49,7 @@
   System/session_manager.scala
   System/standard_system.scala
   System/swing_thread.scala
+  System/system_channel.scala
   Thy/completion.scala
   Thy/html.scala
   Thy/thy_header.scala