lib/scripts/isa-xterm

moved some facts about Pi from ex/PiSets to Fun.ML

#!/bin/bash
#
# $Id$
#
# Simple Isabelle interface based on xterm.


## diagnostics

PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [--] [CMDLINE]"
  echo
  echo "  Options are:"
  echo "    -g GEOM      main window geometry (default 80x60)"
  echo "    -h MODE      highlight mode, may be false, bold (default), color"
  echo "    -p TEXT      pass text (options etc.) to isabelle session"
  echo "    -s BOOL      symbolic font output? (default true)"
  echo
  echo "  Starts Isabelle within an xterm window. CMDLINE is passed"
  echo "  directly to the isabelle session."
  echo
  exit 1
}

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


## process command line

# options

MAINGEOM="80x60"
HILITE=bold
PASS=""
SYMBOLS="true"

while getopts "g:h:p:s:" OPT
do
  case "$OPT" in
    g)
      MAINGEOM="$OPTARG"
      ;;
    h)
      HILITE="$OPTARG"
      ;;
    p)
      PASS="$PASS $OPTARG"
      ;;
    s)
      SYMBOLS="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


## main

if [ "$HILITE" = bold ]; then
  PASS="-m xterm $PASS"
elif [ "$HILITE" = color ]; then
  PASS="-m xterm_color $PASS"
elif [ -n "$HILITE" -a "$HILITE" != false ]; then
  echo "WARNING: unknown highlight mode '$HILITE'" >&2
fi

if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
  exec xterm -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e $ISABELLE $PASS "$@"
else
  $ISATOOL installfonts
  exec xterm -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
    -xrm "*fontMenu.Label: Isabelle fonts" \
    -xrm "*fontMenu*font1*Label: Large" \
    -xrm "*VT100*font1: isabelle24" \
    -xrm "*fontMenu*font2*Label:" \
    -xrm "*VT100*font2:" \
    -xrm "*fontMenu*font3*Label:" \
    -xrm "*VT100*font3:" \
    -xrm "*fontMenu*font4*Label:" \
    -xrm "*VT100*font4:" \
    -xrm "*fontMenu*font5*Label:" \
    -xrm "*VT100*font5:" \
    -xrm "*fontMenu*font6*Label:" \
    -xrm "*VT100*font6:" \
    -e $ISABELLE -m symbols $PASS "$@"
fi