# HG changeset patch
# User wenzelm
# Date 1478942941 -3600
# Node ID 159ea1055b393dfcf286f2e73e068ef0ca7e663f
# Parent  11d1b4e3af1d7faa93f8513b0880d9d6de4f9f24
back to regular Isabelle tool (reverting abc34a149690);

diff -r 11d1b4e3af1d -r 159ea1055b39 Admin/build_polyml
--- a/Admin/build_polyml	Fri Nov 11 21:26:14 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-#
-# DESCRIPTION: build Poly/ML from sources
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-"$THIS/build" jars || exit $?
-exec "$THIS/../bin/isabelle_java" isabelle.Build_PolyML "$@"
diff -r 11d1b4e3af1d -r 159ea1055b39 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 21:26:14 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 12 10:29:01 2016 +0100
@@ -86,7 +86,7 @@
     def bash(cwd: Path, script: String, echo: Boolean = false): Process_Result =
       progress.bash(
         if (other_bash == "") script else Bash.string(other_bash) + " -c " + Bash.string(script),
-        cwd = cwd.file, env = null, echo = echo)
+        cwd = cwd.file, echo = echo)
 
 
     /* configure and make */
@@ -146,16 +146,16 @@
 
 
 
-  /** command line entry point **/
+  /** Isabelle tool wrapper **/
 
-  def main(args: Array[String])
-  {
-    Command_Line.tool0 {
-      var other_bash = ""
-      var arch_64 = false
-      var sha1_root: Option[Path] = None
+  val isabelle_tool = Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
+    {
+      Command_Line.tool0 {
+        var other_bash = ""
+        var arch_64 = false
+        var sha1_root: Option[Path] = None
 
-      val getopts = Getopts("""
+        val getopts = Getopts("""
 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
 
   Options are:
@@ -166,23 +166,23 @@
   Build Poly/ML in the ROOT directory of its sources, with additional
   CONFIGURE_OPTIONS (e.g. --with-gmp).
 """,
-        "b:" -> (arg => other_bash = arg),
-        "m:" ->
-          {
-            case "32" | "x86" => arch_64 = false
-            case "64" | "x86_64" => arch_64 = true
-            case bad => error("Bad processor architecture: " + quote(bad))
-          },
-        "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
+          "b:" -> (arg => other_bash = arg),
+          "m:" ->
+            {
+              case "32" | "x86" => arch_64 = false
+              case "64" | "x86_64" => arch_64 = true
+              case bad => error("Bad processor architecture: " + quote(bad))
+            },
+          "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
 
-      val more_args = getopts(args)
-      val (root, options) =
-        more_args match {
-          case root :: options => (Path.explode(root), options)
-          case Nil => getopts.usage()
-        }
-      build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
-        arch_64 = arch_64, options = options, other_bash = other_bash)
-    }
-  }
+        val more_args = getopts(args)
+        val (root, options) =
+          more_args match {
+            case root :: options => (Path.explode(root), options)
+            case Nil => getopts.usage()
+          }
+        build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
+          arch_64 = arch_64, options = options, other_bash = other_bash)
+      }
+    })
 }
diff -r 11d1b4e3af1d -r 159ea1055b39 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Nov 11 21:26:14 2016 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sat Nov 12 10:29:01 2016 +0100
@@ -101,6 +101,7 @@
     List(
       Build.isabelle_tool,
       Build_Doc.isabelle_tool,
+      Build_PolyML.isabelle_tool,
       Build_Stats.isabelle_tool,
       Check_Sources.isabelle_tool,
       Doc.isabelle_tool,