# HG changeset patch
# User wenzelm
# Date 1457386843 -3600
# Node ID 56449c2d20dbe8f38a59146b83488d1ae3a262d3
# Parent  d2e0d626fb964b88b166c23912a344e148194ffe
prospective command line entry point for simplified isabelle_process;

diff -r d2e0d626fb96 -r 56449c2d20db src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Mar 07 22:37:31 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Mon Mar 07 22:40:43 2016 +0100
@@ -26,6 +26,49 @@
 
     new Isabelle_Process(receiver, system_channel, system_process)
   }
+
+
+  /* command line entry point */
+
+  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()
+
+      val getopts = Getopts("""
+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
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+
+  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
+  $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),
+        "o:" -> (arg => options = options + arg))
+
+      val heap =
+        getopts(args) match {
+          case Nil => ""
+          case List(heap) => heap
+          case _ => getopts.usage()
+        }
+
+      ML_Process(options, heap = heap, args = ml_args, secure = secure, modes = modes).
+        result().print_stdout.rc
+    }
+  }
 }
 
 class Isabelle_Process private(