lib/scripts/isa-emacs

Now if_weak_cong is a standard congruence rule

#!/bin/bash
#
# $Id$
#
# Emacs Isamode interface wrapper.


## diagnostics

PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -g GEOM      main window geometry (default none)"
  echo "    -p NAME      Emacs program name (default xemacs)"
  echo "    -u BOOL      use .emacs file (default false)"
  echo
  echo "Starts Emacs and Isamode."
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

MAINGEOM=""
PROGNAME=xemacs
INITFILE=false

function getoptions()
{
  OPTIND=1
  while getopts "g:p:u:" OPT
  do
    case "$OPT" in
      g)
        MAINGEOM="$OPTARG"
        ;;
      p)
        PROGNAME="$OPTARG"
        ;;
      u)
        INITFILE="$OPTARG"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

getoptions $ISAMODE_OPTIONS

getoptions "$@"
shift $(($OPTIND - 1))


# args

[ $# != 0 ] && usage


## main

ARGS=""

[ -n "$MAINGEOM" ] && ARGS="$ARGS -geometry $MAINGEOM"
[ "$INITFILE" = false ] && ARGS="$ARGS -q"


ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el"

for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \
    "$ISABELLE_HOME_USER/etc/isa-settings.el"
do
  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
done

ARGS="$ARGS -f isabelle"
exec $PROGNAME -T "Isabelle" $ARGS