isabelle: lib/Tools/mkfifo@c01d89d18ff0 (annotated)

28047 8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	1	#!/usr/bin/env bash
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	2	#
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	3	# Author: Makarius
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	4	#
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	5	# DESCRIPTION: create named pipe
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	6
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	7
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	8	PRG="$(basename "$0")"
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	9
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	10	function usage()
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	11	{
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	12	echo
39520 bad14b7d0520 Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process); wenzelm parents: 38253 diff changeset	13	echo "Usage: isabelle $PRG [SUFFIX]"
28047 8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	14	echo
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	15	echo " Create a temporary named pipe and return its name."
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	16	echo
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	17	exit 1
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	18	}
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	19
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	20	function fail()
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	21	{
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	22	echo "$1" >&2
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	23	exit 2
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	24	}
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	25
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	26
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	27	## main
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	28
39520 bad14b7d0520 Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process); wenzelm parents: 38253 diff changeset	29	SUFFIX=""
bad14b7d0520 Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process); wenzelm parents: 38253 diff changeset	30	[ "$#" != 0 ] && { SUFFIX="-$1"; shift; }
bad14b7d0520 Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process); wenzelm parents: 38253 diff changeset	31
28047 8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	32	[ "$#" != 0 ] && usage
8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	33
39521 7ed922d15827 mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default; wenzelm parents: 39520 diff changeset	34	ID="$PPID"
7ed922d15827 mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default; wenzelm parents: 39520 diff changeset	35	[ "$ID" = 0 -o "$ID" = 1 ] && ID="$$" # Cygwin workaround
7ed922d15827 mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default; wenzelm parents: 39520 diff changeset	36
7ed922d15827 mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default; wenzelm parents: 39520 diff changeset	37	FIFO="/tmp/isabelle-fifo${ID}${SUFFIX}"
38253 3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol); wenzelm parents: 29143 diff changeset	38
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol); wenzelm parents: 29143 diff changeset	39	mkfifo -m 600 "$FIFO" \|\| fail "Failed to create fifo: $FIFO"
28047 8dcf4349cf6f create named pipe; wenzelm parents: diff changeset	40	echo "$FIFO"

author	wenzelm
	Sun, 19 Sep 2010 22:40:22 +0200
changeset 39528	c01d89d18ff0
parent 39521	7ed922d15827
permissions	-rwxr-xr-x