# HG changeset patch
# User wenzelm
# Date 1459716871 -7200
# Node ID 1a9ce1b13b20467d2050126dd193bd6e23667e15
# Parent  970cedec97485222e2d483fb25e7960858483249
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;

diff -r 970cedec9748 -r 1a9ce1b13b20 lib/Tools/process
--- a/lib/Tools/process	Sun Apr 03 22:45:40 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: raw ML process (batch mode)
-
-isabelle_admin_build jars || exit $?
-
-case "$ISABELLE_JAVA_PLATFORM" in
-  x86-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
-    ;;
-  x86_64-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
-    ;;
-esac
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-
-exec isabelle java isabelle.ML_Process "$@"
diff -r 970cedec9748 -r 1a9ce1b13b20 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:45:40 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:54:31 2016 +0200
@@ -71,6 +71,7 @@
   register(Build.isabelle_tool)
   register(Check_Sources.isabelle_tool)
   register(Doc.isabelle_tool)
+  register(ML_Process.isabelle_tool)
   register(Options.isabelle_tool)
 
 
diff -r 970cedec9748 -r 1a9ce1b13b20 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sun Apr 03 22:45:40 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Sun Apr 03 22:54:31 2016 +0200
@@ -102,18 +102,17 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
   {
-    Command_Line.tool {
-      var dirs: List[Path] = Nil
-      var eval_args: List[String] = Nil
-      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
-      var modes: List[String] = Nil
-      var options = Options.init()
+    var dirs: List[Path] = Nil
+    var eval_args: List[String] = Nil
+    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+    var modes: List[String] = Nil
+    var options = Options.init()
 
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle process [OPTIONS]
 
   Options are:
@@ -127,20 +126,19 @@
 
   Run the raw Isabelle ML process in batch mode.
 """,
-        "T:" -> (arg =>
-          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
-        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
-        "l:" -> (arg => logic = arg),
-        "m:" -> (arg => modes = arg :: modes),
-        "o:" -> (arg => options = options + arg))
+      "T:" -> (arg =>
+        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+      "l:" -> (arg => logic = arg),
+      "m:" -> (arg => modes = arg :: modes),
+      "o:" -> (arg => options = options + arg))
 
-      val more_args = getopts(args)
-      if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+    val more_args = getopts(args)
+    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
 
-      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
-        result().print_stdout.rc
-    }
-  }
+    ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
+      result().print_stdout.rc
+  })
 }