simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
removed incomprehensible args parser setup;
removed obsolete locale flag -- text is already localized;
misc tuning and cleanup of concrete antiquotations;
goal state antiquotations: ignore source flag;
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: simple XML to YXML converter
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG"
echo
echo " Convert XML (stdin) to YXML (stdout)."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
[ "$#" -ne 0 ] && usage
## main
exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl"