From 37de2996da5255159703148363b31d001a301300 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Sat, 21 Nov 2009 19:36:07 +0000 Subject: more robust THIS/SUPER: allow spaces; modernized usage, eliminated obsolete options -I, -P, -X, -f; re-interpreted option -x as "unicode symbols"; --- isar/interface | 173 ++++++++++++++++-------------------------------- isar/interface-setup.el | 20 +++--- 2 files changed, 67 insertions(+), 126 deletions(-) (limited to 'isar') diff --git a/isar/interface b/isar/interface index 48802f5d..7df483fa 100644 --- a/isar/interface +++ b/isar/interface @@ -7,8 +7,8 @@ ## self references -THIS=$(cd "$(dirname "$0")"; pwd) -SUPER=$(cd "$THIS/.."; pwd) +THIS="$(cd "$(dirname "$0")"; pwd)" +SUPER="$(cd "$THIS/.."; pwd)" ## diagnostics @@ -16,16 +16,11 @@ SUPER=$(cd "$THIS/.."; pwd) usage() { echo - echo "Usage: Isabelle [OPTIONS] [FILES ...]" + echo "Usage: isabelle emacs [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 " -U BOOL enable UTF-8 communication (default true)" 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)" @@ -33,7 +28,7 @@ usage() 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 " -x BOOL render Isabelle symbols via Unicode (default false)" echo echo "Starts Proof General for Isabelle with theory and proof FILES" echo "(default Scratch.thy)." @@ -55,44 +50,29 @@ fail() # options ISABELLE_OPTIONS="" -ISAR="true" -START_PG="true" -GEOMETRY="" + KEYWORDS="" LOGIC="$ISABELLE_LOGIC" +UNICODE="" +GEOMETRY="" PROGNAME="emacs" INITFILE="true" WINDOWSYSTEM="true" -XSYMBOL="" -XSYMBOL_SETUP=true -XSYMBOL_FONTSIZE="12" -UNICODE="" +UNICODE_SYMBOLS="" getoptions() { OPTIND=1 - while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT + while getopts "L:U: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" ;; @@ -119,7 +99,7 @@ getoptions() WINDOWSYSTEM="$OPTARG" ;; x) - XSYMBOL="$OPTARG" + UNICODE_SYMBOLS="$OPTARG" ;; \?) usage @@ -149,104 +129,67 @@ else 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 -if [ "$START_PG" = false ]; then - - [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" - exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC" +declare -a ARGS=() -else +if [ -n "$GEOMETRY" ]; then + ARGS["${#ARGS[@]}"]="-geometry" + ARGS["${#ARGS[@]}"]="$GEOMETRY" +fi - declare -a ARGS=() +[ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" +[ "$WINDOWSYSTEM" = false ] && ARGS["${#ARGS[@]}"]="-nw" - if [ -n "$GEOMETRY" ]; then - ARGS["${#ARGS[@]}"]="-geometry" - ARGS["${#ARGS[@]}"]="$GEOMETRY" - fi +ARGS["${#ARGS[@]}"]="-l" +ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" - [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" - - if [ "$WINDOWSYSTEM" = false ]; then - ARGS["${#ARGS[@]}"]="-nw" - XSYMBOL=false - elif [ -z "$DISPLAY" ]; then - XSYMBOL=false +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 - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts + fail "No isar-keywords file for '$KEYWORDS'" fi - +elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then 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[@]}"]="$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[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" + ARGS["${#ARGS[@]}"]="$FILE" fi +done - 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 - case "$LOGIC" in - /*) - ;; - */*) - LOGIC="$(pwd -P)/$LOGIC" - ;; - esac +export PROOFGENERAL_HOME="$SUPER" +export PROOFGENERAL_ASSISTANTS="isar" +export PROOFGENERAL_LOGIC="$LOGIC" +export PROOFGENERAL_UNICODE="$UNICODE" +export PROOFGENERAL_UNICODE_SYMBOLS="$UNICODE_SYMBOLS" - export PROOFGENERAL_HOME="$SUPER" - export PROOFGENERAL_ASSISTANTS="isar" - export PROOFGENERAL_LOGIC="$LOGIC" - export PROOFGENERAL_XSYMBOL="$XSYMBOL" - export PROOFGENERAL_UNICODE="$UNICODE" +export ISABELLE_OPTIONS - export ISABELLE_OPTIONS XSYMBOL_FONTSIZE +# Isabelle2008 compatibility +[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" +[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" - # Isabelle2008 compatibility - [ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" - [ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" +exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" - exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" - -fi diff --git a/isar/interface-setup.el b/isar/interface-setup.el index effb3541..b2619800 100644 --- a/isar/interface-setup.el +++ b/isar/interface-setup.el @@ -10,16 +10,6 @@ ;; interface-setup.el,v 7.0 2002/08/29 09:14:03 da Exp ;; -;; -;; X-Symbol -- backwards compatibility -;; - -(let ((xsymbol (getenv "PROOFGENERAL_XSYMBOL"))) - - ;; tell Proof General about -x option - (if (and xsymbol (not (equal xsymbol ""))) - (customize-set-variable 'isar-unicode-tokens-enable (equal xsymbol "true")))) - ;; ;; Unicode ;; @@ -29,7 +19,15 @@ (customize-set-variable 'proof-shell-unicode (equal unicode "true")))) ;; -;; Proof General +;; Unicode symbols +;; + +(let ((symbols (getenv "PROOFGENERAL_UNICODE_SYMBOLS"))) + (if (and symbols (not (equal symbols ""))) + (customize-set-variable 'isar-unicode-tokens-enable (equal symbols "true")))) + +;; +;; Proof General startup ;; (if (not (featurep 'proof-site)) -- cgit v1.2.3