simplified Isabelle_System.mk_fifo: inlined script, append PPID and PID uniformly;

--- a/lib/Tools/mkfifo	Sun Sep 19 22:40:22 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: create named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [SUFFIX]"
-  echo
-  echo "  Create a temporary named pipe and return its name."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## main
-
-SUFFIX=""
-[ "$#" != 0 ] && { SUFFIX="-$1"; shift; }
-
-[ "$#" != 0 ] && usage
-
-ID="$PPID"
-[ "$ID" = 0 -o "$ID" = 1 ] && ID="$$"  # Cygwin workaround
-
-FIFO="/tmp/isabelle-fifo${ID}${SUFFIX}"
-
-mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
-echo "$FIFO"

--- a/src/Pure/System/isabelle_system.scala	Sun Sep 19 22:40:22 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Sep 19 23:38:34 2010 +0200
@@ -282,8 +282,13 @@
 
   def mk_fifo(): String =
   {
-    val (result, rc) = isabelle_tool("mkfifo", next_fifo())
-    if (rc == 0) result.trim
+    val i = next_fifo()
+    val script =
+      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
+      "mkfifo -m 600 \"$FIFO\" || { echo \"Failed to create fifo: $FIFO\" >&2; exit 2; }\n" +
+      "echo -n \"$FIFO\"\n"
+    val (result, rc) = bash_output(script)
+    if (rc == 0) result
     else error(result)
   }