undeleted;

1 files changed, 241 insertions, 0 deletions

diff --git a/isa/interface b/isa/interface
new file mode 100644
index 00000000..a562f41e
--- /dev/null
+++ b/isa/interface
@@ -0,0 +1,241 @@
+#!/usr/bin/env bash
+#
+# $Id$
+#
+# Proof General interface wrapper for Isabelle.
+
+
+## self references
+
+THIS=$(cd "$(dirname "$0")"; pwd)
+SUPER=$(cd "$THIS/.."; pwd)
+KIND=$(basename "$(dirname "$0")")
+
+if [ "$KIND" = isar ]; then
+  ISAR=true
+else
+  ISAR=false
+fi
+
+
+## diagnostics
+
+usage()
+{
+  echo
+  echo "Usage: Isabelle [OPTIONS] [FILES ...]"
+  echo
+  echo "  Options are:"
+  echo "    -I BOOL      use Isabelle/Isar instead of classic Isabelle (default $ISAR)"
+  echo "    -P BOOL      actually start Proof General (default true), otherwise"
+  echo "                 run plain tty session"
+  echo "    -X BOOL      configure the X-Symbol package on startup (default true)"
+  echo "    -f SIZE      set X-Symbol font size (default 14)"
+  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 xemacs)"
+  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=""
+START_PG="true"
+GEOMETRY=""
+KEYWORDS=""
+LOGIC="$ISABELLE_LOGIC"
+PROGNAME="xemacs"
+INITFILE="true"
+WINDOWSYSTEM="true"
+XSYMBOL=""
+XSYMBOLSETUP=true
+XSYMBOL_FONTSIZE="12"
+
+getoptions()
+{
+  OPTIND=1
+  while getopts "I:P:X:f:g:k:l:m:p:u:w:x:" OPT
+  do
+    case "$OPT" in
+      I)
+        ISAR="$OPTARG"
+        ;;
+      P)
+        START_PG="$OPTARG"
+        ;;
+      X)
+        XSYMBOLSETUP="$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
+}
+
+getoptions $PROOFGENERAL_OPTIONS
+
+getoptions "$@"
+shift $(($OPTIND - 1))
+
+if [ "$ISAR" = true ]; then
+  KIND=isar
+  DEFAULT_FILES="Scratch.thy"
+else
+  KIND=isa
+  DEFAULT_FILES="Scratch.thy Scratch.ML"
+fi
+
+
+# args
+
+if [ "$#" -eq 0 ]; then
+  FILES="$DEFAULT_FILES"
+else
+  FILES=""
+  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
+
+if [ "$START_PG" = false ]; then
+
+  [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
+  exec "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC"
+
+else
+
+  ARGS=""
+
+  [ -n "$GEOMETRY" ] && ARGS="$ARGS -geometry '$GEOMETRY'"
+
+  [ "$INITFILE" = false ] && ARGS="$ARGS -q"
+  
+  if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
+    #ARGS="$ARGS -T Isabelle"
+    [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && installfonts
+  else
+    ARGS="$ARGS -nw"
+    XSYMBOL=false
+  fi
+  
+  [ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME=""
+  
+  
+  ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'"
+
+  if [ -n "$KEYWORDS" ]; then
+    if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
+      ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el'"
+    elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
+      ARGS="$ARGS -l '$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 '$ISABELLE_HOME_USER/etc/isar-keywords.el'"
+  elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
+    ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords.el'"
+  fi
+  
+  for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
+      "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
+  do
+    [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'"
+  done
+  
+  case "$LOGIC" in
+    /*)
+      ;;
+    */*)
+      LOGIC="$PWD/$LOGIC"
+      ;;
+  esac
+  
+  PROOFGENERAL_HOME="$SUPER"
+  PROOFGENERAL_ASSISTANTS="$KIND"
+  PROOFGENERAL_LOGIC="$LOGIC"
+  PROOFGENERAL_XSYMBOL="$XSYMBOL"
+  
+  export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL
+  export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
+  
+  eval exec "$PROGNAME" "$ARGS" "$FILES"
+
+fi
\ No newline at end of file