# HG changeset patch
# User wenzelm
# Date 921081995 -3600
# Node ID 9442bc6763f7a0d0550fce8dad35d555f9eec793
# Parent  97c697a32b73f5ed5e298cd87f92a067040c8eb8
-x option;

diff -r 97c697a32b73 -r 9442bc6763f7 lib/scripts/isa-xterm
--- a/lib/scripts/isa-xterm	Wed Mar 10 16:31:33 1999 +0100
+++ b/lib/scripts/isa-xterm	Wed Mar 10 17:06:35 1999 +0100
@@ -19,6 +19,7 @@
   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 "    -x PRG       executable program (default xterm)"
   echo
   echo "  Starts Isabelle within an xterm window. CMDLINE is passed"
   echo "  directly to the isabelle session."
@@ -41,11 +42,12 @@
 HILITE=bold
 PASS=""
 SYMBOLS="true"
+XTERM="xterm"
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "g:h:p:s:" OPT
+  while getopts "g:h:p:s:x:" OPT
   do
     case "$OPT" in
       g)
@@ -60,6 +62,9 @@
       s)
         SYMBOLS="$OPTARG"
         ;;
+      x)
+        XTERM="$OPTARG"
+        ;;
       \?)
         usage
         ;;
@@ -84,10 +89,10 @@
 fi
 
 if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
-  exec xterm -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e $ISABELLE $PASS "$@"
+  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e $ISABELLE $PASS "$@"
 else
   $ISATOOL installfonts
-  exec xterm -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
+  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
     -xrm "*fontMenu.Label: Isabelle fonts" \
     -xrm "*fontMenu*font1*Label: Large" \
     -xrm "*VT100*font1: isabelle24" \