# HG changeset patch
# User wenzelm
# Date 1478860874 -3600
# Node ID abc34a149690e395ce8925fd0ca2e0a2d80c38af
# Parent  db1bc27325543dc324f4f522975035623bb3404f
prefer raw Admin tool, without Isabelle settings environment;

diff -r db1bc2732554 -r abc34a149690 Admin/build_polyml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/build_polyml	Fri Nov 11 11:41:14 2016 +0100
@@ -0,0 +1,8 @@
+#!/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 db1bc2732554 -r abc34a149690 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 11:30:31 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 11 11:41:14 2016 +0100
@@ -108,16 +108,15 @@
   }
 
 
-  /* Isabelle tool wrapper */
+  /** command line entry point **/
 
-  val isabelle_tool =
-    Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
-    {
-      Command_Line.tool0 {
-        var other_bash = ""
-        var platform = default_platform
+  def main(args: Array[String])
+  {
+    Command_Line.tool0 {
+      var other_bash = ""
+      var platform = default_platform
 
-        val getopts = Getopts("""
+      val getopts = Getopts("""
 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
 
   Options are:
@@ -127,17 +126,17 @@
   Build Poly/ML in its source ROOT directory of its sources, with additional
   CONFIGURE_OPTIONS (e.g. --with-gmp).
 """,
-          "b:" -> (arg => other_bash = arg),
-          "p:" -> (arg => platform = arg))
+        "b:" -> (arg => other_bash = arg),
+        "p:" -> (arg => platform = 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, progress = new Console_Progress, platform = platform, options = options,
-            other_bash = other_bash)
-      }
-    }, admin = true)
+      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, progress = new Console_Progress, platform = platform, options = options,
+          other_bash = other_bash)
+    }
+  }
 }
diff -r db1bc2732554 -r abc34a149690 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Nov 11 11:30:31 2016 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Fri Nov 11 11:41:14 2016 +0100
@@ -101,7 +101,6 @@
     List(
       Build.isabelle_tool,
       Build_Doc.isabelle_tool,
-      Build_PolyML.isabelle_tool,
       Build_Stats.isabelle_tool,
       Check_Sources.isabelle_tool,
       Doc.isabelle_tool,