diff -r 14873e42659c -r 059926d1d074 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