Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);

--- a/src/Pure/System/isabelle_process.ML	Sun Sep 19 23:38:34 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Sep 20 11:38:14 2010 +0200
@@ -94,21 +94,14 @@
       (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
   in loop end;
 
-fun rendezvous f fifo =
-  let
-    val path = File.platform_path (Path.explode fifo);
-    val result = f fifo;  (*should block until peer is ready*)
-    val _ =
-      if String.isSuffix "cygwin" ml_platform then ()  (*Cygwin 1.7: no proper blocking on open*)
-      else OS.FileSys.remove path;  (*prevent future access*)
-  in result end;
-
 in
 
 fun setup_channels in_fifo out_fifo =
   let
-    val in_stream = rendezvous TextIO.openIn in_fifo;
-    val out_stream = rendezvous TextIO.openOut out_fifo;
+    (*rendezvous*)
+    val in_stream = TextIO.openIn in_fifo;
+    val out_stream = TextIO.openOut out_fifo;
+
     val _ = Simple_Thread.fork false (auto_flush out_stream);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);

--- a/src/Pure/System/isabelle_process.scala	Sun Sep 19 23:38:34 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 11:38:14 2010 +0200
@@ -133,8 +133,13 @@
 
       standard_input = stdin_actor()
       stdout_actor()
-      command_input = input_actor()
-      message_actor()
+
+      // rendezvous
+      val command_stream = system.fifo_output_stream(in_fifo)
+      val message_stream = system.fifo_input_stream(out_fifo)
+
+      command_input = input_actor(command_stream)
+      message_actor(message_stream)
 
       val rc = proc.waitFor()
       Thread.sleep(300)  // FIXME !?
@@ -158,6 +163,7 @@
   private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {
     if (pid.isEmpty && kind == Markup.INIT) {
+      rm_fifos()
       props.find(_._1 == Markup.PID).map(_._1) match {
         case None => system_result("Bad Isabelle process initialization: missing pid")
         case p => pid = p
@@ -277,11 +283,11 @@
 
   /* command input */
 
-  private def input_actor(): Actor =
+  private def input_actor(raw_stream: OutputStream): Actor =
   {
     val name = "command_input"
     Simple_Thread.actor(name) {
-      val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo))
+      val stream = new BufferedOutputStream(raw_stream)
       var finished = false
       while (!finished) {
         try {
@@ -308,14 +314,13 @@
 
   /* message output */
 
-  private def message_actor(): Actor =
+  private def message_actor(stream: InputStream): Actor =
   {
     class EOF extends Exception
     class Protocol_Error(msg: String) extends Exception(msg)
 
     val name = "message_output"
     Simple_Thread.actor(name) {
-      val stream = system.fifo_input_stream(out_fifo)
       val default_buffer = new Array[Byte](65536)
       var c = -1