some document antiquotations for Isabelle/jEdit elements;
modernized theory setup;
#!/usr/bin/env bash
#
# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
#
# Proof General interface wrapper for Isabelle.
## self references
THIS="$(cd "$(dirname "$0")"; pwd)"
SUPER="$(cd "$THIS/.."; pwd)"
## diagnostics
usage()
{
echo
echo "Usage: Isabelle [OPTIONS] [FILES ...]"
echo
echo " Options are:"
echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
echo " -L NAME abbreviates -l NAME -k NAME"
echo " -P BOOL actually start Proof General (default true), otherwise"
echo " run plain tty session"
echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
echo " -X BOOL configure the X-Symbol package on startup (default true)"
echo " -f SIZE set X-Symbol font size (default 12)"
echo " -g GEOMETRY specify Emacs geometry"
echo " -k NAME use specific isar-keywords for named logic"
echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
echo " -m MODE add print mode for output"
echo " -p NAME Emacs program name (default emacs)"
echo " -u BOOL use personal .emacs file (default true)"
echo " -w BOOL use window system (default true)"
echo " -x BOOL enable the X-Symbol package on startup (default false)"
echo
echo "Starts Proof General for Isabelle with theory and proof FILES"
echo "(default Scratch.thy)."
echo
echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
echo
exit 1
}
fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
ISABELLE_OPTIONS=""
ISAR="true"
START_PG="true"
GEOMETRY=""
KEYWORDS=""
LOGIC="$ISABELLE_LOGIC"
PROGNAME="emacs"
INITFILE="true"
WINDOWSYSTEM="true"
XSYMBOL=""
XSYMBOL_SETUP=true
XSYMBOL_FONTSIZE="12"
UNICODE=""
getoptions()
{
OPTIND=1
while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
do
case "$OPT" in
I)
ISAR="$OPTARG"
;;
L)
KEYWORDS="$OPTARG"
LOGIC="$OPTARG"
;;
P)
START_PG="$OPTARG"
;;
U)
UNICODE="$OPTARG"
;;
X)
XSYMBOL_SETUP="$OPTARG"
;;
f)
XSYMBOL_FONTSIZE="$OPTARG"
;;
g)
GEOMETRY="$OPTARG"
;;
k)
KEYWORDS="$OPTARG"
;;
l)
LOGIC="$OPTARG"
;;
m)
if [ -z "$ISABELLE_OPTIONS" ]; then
ISABELLE_OPTIONS="-m $OPTARG"
else
ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
fi
;;
p)
PROGNAME="$OPTARG"
;;
u)
INITFILE="$OPTARG"
;;
w)
WINDOWSYSTEM="$OPTARG"
;;
x)
XSYMBOL="$OPTARG"
;;
\?)
usage
;;
esac
done
}
eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
getoptions "${OPTIONS[@]}"
getoptions "$@"
shift $(($OPTIND - 1))
# args
declare -a FILES=()
if [ "$#" -eq 0 ]; then
FILES["${#FILES[@]}"]="Scratch.thy"
else
while [ "$#" -gt 0 ]; do
FILES["${#FILES[@]}"]="$1"
shift
done
fi
## smart X11 font installation
function checkfonts ()
{
XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
case "$XLSFONTS" in
xlsfonts:*)
return 1
;;
esac
return 0
}
function installfonts ()
{
checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
}
## main
# Isabelle2008 compatibility
[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
if [ "$START_PG" = false ]; then
[ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
else
declare -a ARGS=()
if [ -n "$GEOMETRY" ]; then
ARGS["${#ARGS[@]}"]="-geometry"
ARGS["${#ARGS[@]}"]="$GEOMETRY"
fi
[ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
if [ "$WINDOWSYSTEM" = false ]; then
ARGS["${#ARGS[@]}"]="-nw"
XSYMBOL=false
elif [ -z "$DISPLAY" ]; then
XSYMBOL=false
else
[ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
fi
if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
then
if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
then
cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
sleep 3
fi
fi
ARGS["${#ARGS[@]}"]="-l"
ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
if [ -n "$KEYWORDS" ]; then
if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
ARGS["${#ARGS[@]}"]="-l"
ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
ARGS["${#ARGS[@]}"]="-l"
ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
else
fail "No isar-keywords file for '$KEYWORDS'"
fi
elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
ARGS["${#ARGS[@]}"]="-l"
ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
ARGS["${#ARGS[@]}"]="-l"
ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
fi
for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
"$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
do
if [ -f "$FILE" ]; then
ARGS["${#ARGS[@]}"]="-l"
ARGS["${#ARGS[@]}"]="$FILE"
fi
done
case "$LOGIC" in
/*)
;;
*/*)
LOGIC="$(pwd -P)/$LOGIC"
;;
esac
export PROOFGENERAL_HOME="$SUPER"
export PROOFGENERAL_ASSISTANTS="isar"
export PROOFGENERAL_LOGIC="$LOGIC"
export PROOFGENERAL_XSYMBOL="$XSYMBOL"
export PROOFGENERAL_UNICODE="$UNICODE"
export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
fi