lib/scripts/isa-xterm
author wenzelm
Sat, 24 Nov 2001 16:54:32 +0100
changeset 12282 f98beaaa7c4f
parent 10555 2323ec838401
permissions -rwxr-xr-x
generic_merge;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10512
diff changeset
     1
#!/usr/bin/env 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$
9789
wenzelm
parents: 8598
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 8598
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2300
diff changeset
     6
#
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
     7
# Simple Isabelle interface based on xterm.
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     8
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
     9
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    10
## diagnostics
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    11
10512
wenzelm
parents: 9794
diff changeset
    12
PRG="$(basename "$0")"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    13
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    14
function usage()
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    15
{
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    16
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    17
  echo "Usage: $PRG [OPTIONS] [--] [CMDLINE]"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    18
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    19
  echo "  Options are:"
8598
f625793c4fff -I option;
wenzelm
parents: 7459
diff changeset
    20
  echo "    -I           startup Isar interaction mode"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    21
  echo "    -g GEOM      main window geometry (default 80x60)"
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    22
  echo "    -h MODE      highlight mode, may be false, bold (default), color"
7206
012d8defdaa3 -m option;
wenzelm
parents: 6344
diff changeset
    23
  echo "    -m MODE      pass print mode"
2712
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    24
  echo "    -p TEXT      pass text (options etc.) to isabelle session"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    25
  echo "    -s BOOL      symbolic font output? (default true)"
6344
9442bc6763f7 -x option;
wenzelm
parents: 6277
diff changeset
    26
  echo "    -x PRG       executable program (default xterm)"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    27
  echo
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    28
  echo "  Starts Isabelle within an xterm window. CMDLINE is passed"
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    29
  echo "  directly to the isabelle session."
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    30
  echo
7459
173efad74891 usage: tell current OPTIONS value;
wenzelm
parents: 7241
diff changeset
    31
  echo "  ISABELLE_XTERM_OPTIONS=$ISABELLE_XTERM_OPTIONS"
173efad74891 usage: tell current OPTIONS value;
wenzelm
parents: 7241
diff changeset
    32
  echo
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    33
  exit 1
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    34
}
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    35
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    36
function fail()
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    37
{
2344
c3e1eaea4418 added -norc option;
wenzelm
parents: 2315
diff changeset
    38
  echo "$1" >&2
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    39
  exit 2
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    40
}
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    41
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    42
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    43
## process command line
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    44
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    45
# options
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    46
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    47
MAINGEOM="80x60"
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    48
HILITE=bold
2712
44a657985de1 removed -r option;
wenzelm
parents: 2702
diff changeset
    49
PASS=""
7206
012d8defdaa3 -m option;
wenzelm
parents: 6344
diff changeset
    50
PASS_MODE=""
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    51
SYMBOLS="true"
6344
9442bc6763f7 -x option;
wenzelm
parents: 6277
diff changeset
    52
XTERM="xterm"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    53
5965
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    54
function getoptions()
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    55
{
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    56
  OPTIND=1
8598
f625793c4fff -I option;
wenzelm
parents: 7459
diff changeset
    57
  while getopts "Ig:h:m:p:s:x:" OPT
5965
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    58
  do
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    59
    case "$OPT" in
8598
f625793c4fff -I option;
wenzelm
parents: 7459
diff changeset
    60
      I)
f625793c4fff -I option;
wenzelm
parents: 7459
diff changeset
    61
        PASS="$PASS -I"
f625793c4fff -I option;
wenzelm
parents: 7459
diff changeset
    62
        ;;
5965
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    63
      g)
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    64
        MAINGEOM="$OPTARG"
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    65
        ;;
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    66
      h)
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    67
        HILITE="$OPTARG"
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    68
        ;;
7206
012d8defdaa3 -m option;
wenzelm
parents: 6344
diff changeset
    69
      m)
7241
8f3c14d60345 PASS(_MODE): works better without space (why?);
wenzelm
parents: 7206
diff changeset
    70
        PASS_MODE="$PASS_MODE -m$OPTARG"
7206
012d8defdaa3 -m option;
wenzelm
parents: 6344
diff changeset
    71
        ;;
5965
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    72
      p)
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    73
        PASS="$PASS $OPTARG"
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    74
        ;;
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    75
      s)
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    76
        SYMBOLS="$OPTARG"
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    77
        ;;
6344
9442bc6763f7 -x option;
wenzelm
parents: 6277
diff changeset
    78
      x)
9442bc6763f7 -x option;
wenzelm
parents: 6277
diff changeset
    79
        XTERM="$OPTARG"
9442bc6763f7 -x option;
wenzelm
parents: 6277
diff changeset
    80
        ;;
5965
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    81
      \?)
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    82
        usage
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    83
        ;;
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    84
    esac
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    85
  done
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    86
}
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    87
5965
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    88
getoptions $ISABELLE_XTERM_OPTIONS
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    89
f91212fd2c7c eliminated ISABELLE_INTERFACE_OPTIONS;
wenzelm
parents: 3007
diff changeset
    90
getoptions "$@"
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    91
shift $(($OPTIND - 1))
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    92
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
    93
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    94
## main
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
    95
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    96
if [ "$HILITE" = bold ]; then
7241
8f3c14d60345 PASS(_MODE): works better without space (why?);
wenzelm
parents: 7206
diff changeset
    97
  PASS="-mxterm $PASS"
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
    98
elif [ "$HILITE" = color ]; then
7241
8f3c14d60345 PASS(_MODE): works better without space (why?);
wenzelm
parents: 7206
diff changeset
    99
  PASS="-mxterm_color $PASS"
2788
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
   100
elif [ -n "$HILITE" -a "$HILITE" != false ]; then
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
   101
  echo "WARNING: unknown highlight mode '$HILITE'" >&2
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
   102
fi
0178e3cd9714 tuned comments;
wenzelm
parents: 2770
diff changeset
   103
7206
012d8defdaa3 -m option;
wenzelm
parents: 6344
diff changeset
   104
PASS="$PASS_MODE $PASS"
012d8defdaa3 -m option;
wenzelm
parents: 6344
diff changeset
   105
2623
6a7372c9ca0f improved interface options;
wenzelm
parents: 2474
diff changeset
   106
if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9789
diff changeset
   107
  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e "$ISABELLE" $PASS "$@"
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
   108
else
2474
9990f088d7ac minor tuning;
wenzelm
parents: 2430
diff changeset
   109
  $ISATOOL installfonts
6344
9442bc6763f7 -x option;
wenzelm
parents: 6277
diff changeset
   110
  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
2743
wenzelm
parents: 2713
diff changeset
   111
    -xrm "*fontMenu.Label: Isabelle fonts" \
wenzelm
parents: 2713
diff changeset
   112
    -xrm "*fontMenu*font1*Label: Large" \
2770
5a3224f488db renamed font;
wenzelm
parents: 2743
diff changeset
   113
    -xrm "*VT100*font1: isabelle24" \
2743
wenzelm
parents: 2713
diff changeset
   114
    -xrm "*fontMenu*font2*Label:" \
wenzelm
parents: 2713
diff changeset
   115
    -xrm "*VT100*font2:" \
wenzelm
parents: 2713
diff changeset
   116
    -xrm "*fontMenu*font3*Label:" \
wenzelm
parents: 2713
diff changeset
   117
    -xrm "*VT100*font3:" \
wenzelm
parents: 2713
diff changeset
   118
    -xrm "*fontMenu*font4*Label:" \
wenzelm
parents: 2713
diff changeset
   119
    -xrm "*VT100*font4:" \
wenzelm
parents: 2713
diff changeset
   120
    -xrm "*fontMenu*font5*Label:" \
wenzelm
parents: 2713
diff changeset
   121
    -xrm "*VT100*font5:" \
wenzelm
parents: 2713
diff changeset
   122
    -xrm "*fontMenu*font6*Label:" \
wenzelm
parents: 2713
diff changeset
   123
    -xrm "*VT100*font6:" \
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9789
diff changeset
   124
    -e "$ISABELLE" -m isabelle_font -m symbols $PASS "$@"
2300
9af0cf87ac48 isa-xterm: Isabelle within an xterm.
wenzelm
parents:
diff changeset
   125
fi