# HG changeset patch
# User wenzelm
# Date 910606846 -3600
# Node ID b4d4a97df4380702e7e80828ed13d9285ce7bba3
# Parent  a3881c1f1d3c5388673811037dc77b245cd12879
option -I: startup Isar interaction mode;

diff -r a3881c1f1d3c -r b4d4a97df438 bin/isabelle
--- a/bin/isabelle	Mon Nov 09 11:20:07 1998 +0100
+++ b/bin/isabelle	Mon Nov 09 11:20:46 1998 +0100
@@ -22,6 +22,7 @@
   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
   echo
   echo "  Options are:"
+  echo "    -I           startup Isar interaction mode"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
@@ -54,9 +55,12 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "e:m:qruw" OPT
+while getopts "Ie:m:qruw" OPT
 do
   case "$OPT" in
+    I)
+      MLTEXT="$MLTEXT OuterSyntax.main();"
+      ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;