# HG changeset patch
# User wenzelm
# Date 1457432301 -3600
# Node ID fd6e64133684eb2c741d19ff33c2110b978e2ea7
# Parent  56449c2d20dbe8f38a59146b83488d1ae3a262d3
removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;

diff -r 56449c2d20db -r fd6e64133684 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Mar 07 22:40:43 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Tue Mar 08 11:18:21 2016 +0100
@@ -33,7 +33,6 @@
   def main(args: Array[String])
   {
     Command_Line.tool {
-      var secure = false
       var ml_args: List[String] = Nil
       var modes: List[String] = Nil
       var options = Options.init()
@@ -42,7 +41,6 @@
 Usage: isabelle_process [OPTIONS] [HEAP]
 
   Options are:
-    -S           secure mode -- disallow critical operations
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
     -m MODE      add print mode for output
@@ -52,7 +50,6 @@
   $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
   if it is RAW_ML_SYSTEM, the initial ML heap is used.
 """,
-        "S" -> (_ => secure = true),
         "e:" -> (arg => ml_args = ml_args ::: List("--eval", arg)),
         "f:" -> (arg => ml_args = ml_args ::: List("--use", arg)),
         "m:" -> (arg => modes = arg :: modes),
@@ -65,7 +62,7 @@
           case _ => getopts.usage()
         }
 
-      ML_Process(options, heap = heap, args = ml_args, secure = secure, modes = modes).
+      ML_Process(options, heap = heap, args = ml_args, modes = modes).
         result().print_stdout.rc
     }
   }