IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
IsabelleSystem.exec: varargs convenience;
more robust message thread management: no interrupt, but proper rendezvous via fifo (rm_fifo removes unused fifo, if isabelle-process fails);
#!/usr/bin/env bash
#
# $Id$
# Author: Makarius
#
# DESCRIPTION: remove named pipe
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: $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