added option -S (secure mode);
authorwenzelm
Mon, 09 Oct 2006 19:37:02 +0200
changeset 20923 059926d1d074
parent 20922 14873e42659c
child 20924 fa4930418e5a
added option -S (secure mode);
bin/isabelle-process
--- 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