slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;

--- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 17:11:39 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Sep 18 17:14:47 2010 +0200
@@ -147,9 +147,13 @@
 
   /** stream actors **/
 
-  case class Input_Text(text: String)
-  case class Input_Chunks(chunks: List[Array[Byte]])
-  case object Close
+  private val in_fifo = system.mk_fifo()
+  private val out_fifo = system.mk_fifo()
+  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
+
+  private case class Input_Text(text: String)
+  private case class Input_Chunks(chunks: List[Array[Byte]])
+  private case object Close
 
 
   /* raw stdin */
@@ -220,9 +224,9 @@
 
   /* command input */
 
-  private def input_actor(name: String, raw_stream: OutputStream): Actor =
+  private def input_actor(name: String): Actor =
     Simple_Thread.actor(name) {
-      val stream = new BufferedOutputStream(raw_stream)
+      val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo))  // FIXME potentially blocking forever
       var finished = false
       while (!finished) {
         try {
@@ -252,8 +256,9 @@
 
   private class Protocol_Error(msg: String) extends Exception(msg)
 
-  private def message_actor(name: String, stream: InputStream): Actor =
+  private def message_actor(name: String): Actor =
     Simple_Thread.actor(name) {
+      val stream = system.fifo_input_stream(out_fifo)  // FIXME potentially blocking forever
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
@@ -317,10 +322,6 @@
 
   /* exec process */
 
-  private val in_fifo = system.mk_fifo()
-  private val out_fifo = system.mk_fifo()
-  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
-
   try {
     val cmdline =
       List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
@@ -335,12 +336,12 @@
 
   /* I/O actors */
 
+  private val command_input = input_actor("command_input")
+  message_actor("message_output")
+
   private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
   stdout_actor("standard_output", proc.get.getInputStream)
 
-  private val command_input = input_actor("command_input", system.fifo_output_stream(in_fifo))
-  message_actor("message_output", system.fifo_input_stream(out_fifo))
-
 
   /* exit process */