more robust THIS/SUPER: allow spaces;

modernized usage, eliminated obsolete options -I, -P, -X, -f;
re-interpreted option -x as "unicode symbols";

1 files changed, 58 insertions, 115 deletions

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