# HG changeset patch
# User wenzelm
# Date 1284824363 -7200
# Node ID bad14b7d0520528d8adbb54b25303d9ee66709cd
# Parent  b376f53bcc1859ce3d31f6b30d3f1a28aeb644d4
Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process);

diff -r b376f53bcc18 -r bad14b7d0520 lib/Tools/mkfifo
--- a/lib/Tools/mkfifo	Sat Sep 18 17:14:47 2010 +0200
+++ b/lib/Tools/mkfifo	Sat Sep 18 17:39:23 2010 +0200
@@ -10,7 +10,7 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG"
+  echo "Usage: isabelle $PRG [SUFFIX]"
   echo
   echo "  Create a temporary named pipe and return its name."
   echo
@@ -26,10 +26,12 @@
 
 ## main
 
+SUFFIX=""
+[ "$#" != 0 ] && { SUFFIX="-$1"; shift; }
+
 [ "$#" != 0 ] && usage
 
-#FIXME potential race condition wrt. future processes with same pid
-FIFO="/tmp/isabelle-fifo$$"
+FIFO="/tmp/isabelle-fifo${PPID}${SUFFIX}"
 
 mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
 echo "$FIFO"
diff -r b376f53bcc18 -r bad14b7d0520 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Sep 18 17:14:47 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Sep 18 17:39:23 2010 +0200
@@ -273,9 +273,16 @@
 
   /* named pipes */
 
+  private var fifo_count: Long = 0
+  private def next_fifo(): String = synchronized {
+    require(fifo_count < java.lang.Long.MAX_VALUE)
+    fifo_count += 1
+    fifo_count.toString
+  }
+
   def mk_fifo(): String =
   {
-    val (result, rc) = isabelle_tool("mkfifo")
+    val (result, rc) = isabelle_tool("mkfifo", next_fifo())
     if (rc == 0) result.trim
     else error(result)
   }