removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;
authorwenzelm
Tue Mar 08 11:18:21 2016 +0100 (2016-03-08)
changeset 62555fd6e64133684
parent 62554 56449c2d20db
child 62556 c115e69f457f
removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Mar 07 22:40:43 2016 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Mar 08 11:18:21 2016 +0100
     1.3 @@ -33,7 +33,6 @@
     1.4    def main(args: Array[String])
     1.5    {
     1.6      Command_Line.tool {
     1.7 -      var secure = false
     1.8        var ml_args: List[String] = Nil
     1.9        var modes: List[String] = Nil
    1.10        var options = Options.init()
    1.11 @@ -42,7 +41,6 @@
    1.12  Usage: isabelle_process [OPTIONS] [HEAP]
    1.13  
    1.14    Options are:
    1.15 -    -S           secure mode -- disallow critical operations
    1.16      -e ML_EXPR   evaluate ML expression on startup
    1.17      -f ML_FILE   evaluate ML file on startup
    1.18      -m MODE      add print mode for output
    1.19 @@ -52,7 +50,6 @@
    1.20    $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
    1.21    if it is RAW_ML_SYSTEM, the initial ML heap is used.
    1.22  """,
    1.23 -        "S" -> (_ => secure = true),
    1.24          "e:" -> (arg => ml_args = ml_args ::: List("--eval", arg)),
    1.25          "f:" -> (arg => ml_args = ml_args ::: List("--use", arg)),
    1.26          "m:" -> (arg => modes = arg :: modes),
    1.27 @@ -65,7 +62,7 @@
    1.28            case _ => getopts.usage()
    1.29          }
    1.30  
    1.31 -      ML_Process(options, heap = heap, args = ml_args, secure = secure, modes = modes).
    1.32 +      ML_Process(options, heap = heap, args = ml_args, modes = modes).
    1.33          result().print_stdout.rc
    1.34      }
    1.35    }