--- a/bin/isabelle-process Mon Oct 09 12:51:31 2006 +0200
+++ b/bin/isabelle-process Mon Oct 09 19:37:02 2006 +0200
@@ -30,6 +30,7 @@
echo " -C tell ML system to copy output image"
echo " -I startup Isar interaction mode"
echo " -P startup Proof General interaction mode"
+ echo " -S secure mode -- disallow critical operations (e.g. ML evaluation)"
echo " -X startup PGIP interaction mode"
echo " -c tell ML system to compress output image"
echo " -e MLTEXT pass MLTEXT to the ML session"
@@ -62,6 +63,7 @@
COPYDB=""
ISAR=false
PROOFGENERAL=""
+SECURE=""
COMPRESS=""
MLTEXT=""
MODES=""
@@ -69,7 +71,7 @@
READONLY=""
NOWRITE=""
-while getopts "XCIPce:fm:qruw" OPT
+while getopts "XCIPSce:fm:qruw" OPT
do
case "$OPT" in
C)
@@ -81,6 +83,9 @@
P)
PROOFGENERAL=true
;;
+ S)
+ SECURE=true
+ ;;
X)
PGIP=true
;;
@@ -209,6 +214,8 @@
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
+[ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
+
if [ -n "$PGIP" ]; then
MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
elif [ -n "$PROOFGENERAL" ]; then