some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: view Isabelle documentation
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [DOC ...]"
echo
echo " View Isabelle documentation."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## args
[ "$#" -eq 1 -a "$1" = "-?" ] && usage
## main
isabelle_admin_build jars || exit $?
"$ISABELLE_TOOL" java isabelle.Doc "$@"