# HG changeset patch
# User wenzelm
# Date 1284837007 -7200
# Node ID d8971680b0fc656e06bd70dae3b512c100101c50
# Parent  01aade784da9a1234633e75943ad32e61ae49b35
simplified fifo handling -- rm_fifo always succeeds without ever blocking;
tuned;

diff -r 01aade784da9 -r d8971680b0fc lib/Tools/rmfifo
--- a/lib/Tools/rmfifo	Sat Sep 18 20:07:48 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: remove named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG NAME"
-  echo
-  echo "  Remove an unused named pipe, after producing dummy output"
-  echo "  to unblock the reader (blocks if no reader present)."
-  echo
-  exit 1
-}
-
-
-## main
-
-[ "$#" != 1 ] && usage
-FIFO="$1"; shift
-
-if [ -p "$FIFO" ]; then
-  echo -n "" >"$FIFO" && rm -f "$FIFO"
-fi
diff -r 01aade784da9 -r d8971680b0fc src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 20:07:48 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:10:07 2010 +0200
@@ -147,10 +147,6 @@
 
   /** stream actors **/
 
-  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
@@ -224,9 +220,9 @@
 
   /* command input */
 
-  private def input_actor(name: String): Actor =
+  private def input_actor(name: String, fifo: String): Actor =
     Simple_Thread.actor(name) {
-      val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo))  // FIXME potentially blocking forever
+      val stream = new BufferedOutputStream(system.fifo_output_stream(fifo))  // FIXME potentially blocking forever
       var finished = false
       while (!finished) {
         try {
@@ -256,9 +252,9 @@
 
   private class Protocol_Error(msg: String) extends Exception(msg)
 
-  private def message_actor(name: String): Actor =
+  private def message_actor(name: String, fifo: String): Actor =
     Simple_Thread.actor(name) {
-      val stream = system.fifo_input_stream(out_fifo)  // FIXME potentially blocking forever
+      val stream = system.fifo_input_stream(fifo)  // FIXME potentially blocking forever
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
@@ -322,22 +318,22 @@
 
   /* 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
     proc = Some(system.execute(true, cmdline: _*))
   }
-  catch {
-    case e: IOException =>
-      rm_fifos()
-      error("Failed to execute Isabelle process: " + e.getMessage)
-  }
+  catch { case e: IOException => rm_fifos(); throw(e) }
 
 
   /* I/O actors */
 
-  private val command_input = input_actor("command_input")
-  message_actor("message_output")
+  private val command_input = input_actor("command_input", in_fifo)
+  message_actor("message_output", out_fifo)
 
   private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
   stdout_actor("standard_output", proc.get.getInputStream)
@@ -351,7 +347,7 @@
       case Some(p) =>
         val rc = p.waitFor()
         Thread.sleep(300)  // FIXME property!?
-        put_result(Markup.SYSTEM, "process_exit terminated")
+        put_result(Markup.SYSTEM, "Isabelle process terminated")
         put_result(Markup.EXIT, rc.toString)
     }
     rm_fifos()
diff -r 01aade784da9 -r d8971680b0fc src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Sep 18 20:07:48 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Sep 18 21:10:07 2010 +0200
@@ -289,8 +289,7 @@
 
   def rm_fifo(fifo: String)
   {
-    val (result, rc) = isabelle_tool("rmfifo", fifo)
-    if (rc != 0) error(result)
+    bash_output("rm -f '" + fifo + "'")
   }
 
   def fifo_input_stream(fifo: String): InputStream =