Remove obsolete prefixes from error and warning messages.
#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# Isabelle tool starter.
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi
## settings
PRG="$(basename "$0")"
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics
function usage()
{
echo
echo "Usage: $PRG TOOL [ARGS ...]"
echo
echo " Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
echo " for more specific help."
echo
echo " Available tools are:"
(
ORIG_IFS="$IFS"
IFS=":"
for DIR in $ISABELLE_TOOLS
do
cd "$DIR"
for T in *
do
if [ -f "$T" -a -x "$T" ]; then
DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
echo " $T - $DESCRLINE"
fi
done
done
IFS="$ORIG_IFS"
)
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## args
[ "$#" -lt 1 -o "$1" = "-?" ] && usage
TOOLNAME="$1"
shift
## main
ORIG_IFS="$IFS"
IFS=":"
for DIR in $ISABELLE_TOOLS
do
TOOL="$DIR/$TOOLNAME"
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
done
IFS="$ORIG_IFS"
fail "Unknown Isabelle tool: $TOOLNAME"