diff -r ed9720047d53 -r 9af0cf87ac48 lib/scripts/isa-xterm
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/isa-xterm	Mon Dec 02 18:23:32 1996 +0100
@@ -0,0 +1,26 @@
+#!/bin/bash
+#
+# Isabelle within an xterm.
+#
+# $Id$
+#
+# TODO: isabelle fonts
+
+
+## diagnostics
+
+function fail()
+{
+  echo "$1"
+  exit 2
+}
+
+
+## main
+
+if [ -z "$ISABELLE_SYMBOLS" -o "$ISABELLE_SYMBOLS" = false ]; then
+  exec xterm $ISABELLE_INTERFACE_OPTIONS -e isabelle "$@"
+else
+  isatool installfonts
+  exec xterm $ISABELLE_INTERFACE_OPTIONS -fn isacr14 -e isabelle -e 'print_mode:=["symbols"];' "$@"
+fi