generic Syntax.pretty/string_of operations;
added uncheck/unparse_classrel/arity (from sign.ML);
tuned;
#!/usr/bin/env bash
#
# $Id$
#
# leightweight link checker for the isabelle website
PRG=`basename "$0"`
usage()
{
echo
echo "Usage: $PRG URL"
echo
exit 1
}
fail()
{
echo "$1" >&2
exit 2
}
url="$1"
if [ -z "$url" ]
then
usage;
fi
type -p ggrep > /dev/zero && GREP=ggrep || GREP=grep
mkdir -p /tmp/isa_linktest
dir=$(pwd)
cd /tmp/isa_linktest
exec wget --non-verbose --cookies=off --recursive --reject='GraphBrowser.class' --convert-links --page-requisites \
--delete-after \
"$url" \
2>&1 | tee /tmp/isa_linktest.report | "$GREP" -i -B1 "ERROR"
cd "$dir"
rm -rf /tmp/isa_linktest