Deleted file

1 files changed, 0 insertions, 241 deletions

diff --git a/isa/interface b/isa/interface
deleted file mode 100644
index 73e51d47..00000000
--- a/isa/interface
+++ /dev/null
@@ -1,241 +0,0 @@
-#!/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