# HG changeset patch
# User wenzelm
# Date 857145391 -3600
# Node ID afa01c9f1ab04430f94ae4a2d0bc4e7861547076
# Parent  5ce1310560ffa960fb96703182e460b75d1ad44e
more robust handling of invocation errors;
added -m MODE option;

diff -r 5ce1310560ff -r afa01c9f1ab0 bin/isabelle
--- a/bin/isabelle	Fri Feb 28 16:55:35 1997 +0100
+++ b/bin/isabelle	Fri Feb 28 16:56:31 1997 +0100
@@ -7,14 +7,27 @@
 
 ## settings
 
+PRG=$(basename $0)
+
 ISABELLE_HOME=$(dirname $(dirname $0))
-. $ISABELLE_HOME/lib/scripts/getsettings || exit 2
+case "$ISABELLE_HOME" in
+  /*)
+    if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
+      . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
+    else
+      echo "ERROR: $PRG probably not called from its original place!"
+      exit 1
+    fi
+    ;;
+  *)
+    echo "ERROR: $PRG not called with absolute path specification!"
+    exit 1
+    ;;
+esac
 
 
 ## diagnostics
 
-PRG=$(basename $0)
-
 function usage()
 {
   echo
@@ -23,6 +36,7 @@
   echo "  Options are:"
   echo "    -c           force copying of heap file (for Poly/ML)"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
+  echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
   echo "    -r           open heap file read-only"
   echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
@@ -49,10 +63,11 @@
 COPYDB=""
 MLTEXT=""
 COPYDB=""
+MODES=""
 TERMINATE=""
 READONLY=""
 
-while getopts "ce:qru" OPT
+while getopts "ce:m:qru" OPT
 do
   case "$OPT" in
     c)
@@ -61,6 +76,13 @@
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
+    m)
+      if [ -z "$MODES" ]; then
+        MODES="\"$OPTARG\""
+      else
+        MODES="$MODES, \"$OPTARG\""
+      fi
+      ;;
     q)
       TERMINATE=true
       ;;
@@ -155,6 +177,8 @@
 
 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
 
+[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
+
 export INFILE OUTFILE COPYDB MLTEXT TERMINATE
 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE