lib/scripts/isa-xterm
author berghofe
Thu, 30 Jul 1998 15:49:18 +0200
changeset 5213 0aa62210e67c
parent 3007 e5efa177ee0c
child 5965 f91212fd2c7c
permissions -rwxr-xr-x
Script that adapts theories and proof scripts to new datatype package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2788
diff changeset
     1
#!/bin/bash
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     2
#
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2300
diff changeset
     3
# $Id$
508d2a233dbc *** empty log message ***
wenzelm
parents: 2300
diff changeset
     4
#
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
     5
# Simple Isabelle interface based on xterm.
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     6
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     7
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     8
## diagnostics
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     9
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    10
PRG=$(basename $0)
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    11
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    12
function usage()
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    13
{
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    14
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    15
  echo "Usage: $PRG [OPTIONS] [--] [CMDLINE]"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    16
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    17
  echo "  Options are:"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    18
  echo "    -g GEOM      main window geometry (default 80x60)"
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    19
  echo "    -h MODE      highlight mode, may be false, bold (default), color"
2712
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    20
  echo "    -p TEXT      pass text (options etc.) to isabelle session"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    21
  echo "    -s BOOL      symbolic font output? (default true)"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    22
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    23
  echo "  Starts Isabelle within an xterm window. CMDLINE is passed"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    24
  echo "  directly to the isabelle session."
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    25
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    26
  exit 1
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    27
}
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    28
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    29
function fail()
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    30
{
2344
c3e1eaea4418 added -norc option;
wenzelm
parents: 2315
diff changeset
    31
  echo "$1" >&2
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    32
  exit 2
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    33
}
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    34
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    35
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    36
## process command line
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    37
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    38
# options
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    39
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    40
MAINGEOM="80x60"
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    41
HILITE=bold
2712
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    42
PASS=""
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    43
SYMBOLS="true"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    44
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    45
while getopts "g:h:p:s:" OPT
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    46
do
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    47
  case "$OPT" in
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    48
    g)
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    49
      MAINGEOM="$OPTARG"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    50
      ;;
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    51
    h)
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    52
      HILITE="$OPTARG"
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    53
      ;;
2712
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    54
    p)
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    55
      PASS="$PASS $OPTARG"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    56
      ;;
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    57
    s)
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    58
      SYMBOLS="$OPTARG"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    59
      ;;
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    60
    \?)
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    61
      usage
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    62
      ;;
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    63
  esac
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    64
done
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    65
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    66
shift $(($OPTIND - 1))
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    67
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    68
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    69
## main
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    70
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    71
if [ "$HILITE" = bold ]; then
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    72
  PASS="-m xterm $PASS"
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    73
elif [ "$HILITE" = color ]; then
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    74
  PASS="-m xterm_color $PASS"
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    75
elif [ -n "$HILITE" -a "$HILITE" != false ]; then
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    76
  echo "WARNING: unknown highlight mode '$HILITE'" >&2
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    77
fi
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    78
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    79
if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
2712
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    80
  exec xterm -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e $ISABELLE $PASS "$@"
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    81
else
2474
9990f088d7ac minor tuning;
wenzelm
parents: 2430
diff changeset
    82
  $ISATOOL installfonts
2770
5a3224f488db renamed font;
wenzelm
parents: 2743
diff changeset
    83
  exec xterm -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
2743
wenzelm
parents: 2713
diff changeset
    84
    -xrm "*fontMenu.Label: Isabelle fonts" \
wenzelm
parents: 2713
diff changeset
    85
    -xrm "*fontMenu*font1*Label: Large" \
2770
5a3224f488db renamed font;
wenzelm
parents: 2743
diff changeset
    86
    -xrm "*VT100*font1: isabelle24" \
2743
wenzelm
parents: 2713
diff changeset
    87
    -xrm "*fontMenu*font2*Label:" \
wenzelm
parents: 2713
diff changeset
    88
    -xrm "*VT100*font2:" \
wenzelm
parents: 2713
diff changeset
    89
    -xrm "*fontMenu*font3*Label:" \
wenzelm
parents: 2713
diff changeset
    90
    -xrm "*VT100*font3:" \
wenzelm
parents: 2713
diff changeset
    91
    -xrm "*fontMenu*font4*Label:" \
wenzelm
parents: 2713
diff changeset
    92
    -xrm "*VT100*font4:" \
wenzelm
parents: 2713
diff changeset
    93
    -xrm "*fontMenu*font5*Label:" \
wenzelm
parents: 2713
diff changeset
    94
    -xrm "*VT100*font5:" \
wenzelm
parents: 2713
diff changeset
    95
    -xrm "*fontMenu*font6*Label:" \
wenzelm
parents: 2713
diff changeset
    96
    -xrm "*VT100*font6:" \
wenzelm
parents: 2713
diff changeset
    97
    -e $ISABELLE -m symbols $PASS "$@"
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    98
fi