# HG changeset patch
# User wenzelm
# Date 1478860231 -3600
# Node ID db1bc27325543dc324f4f522975035623bb3404f
# Parent  bc77e19aad44b83af7f4e70c3c30119571c7d662
clarified command-line;

diff -r bc77e19aad44 -r db1bc2732554 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 11:02:31 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 11 11:30:31 2016 +0100
@@ -55,13 +55,14 @@
   lazy val default_platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM32")
 
   def build_polyml(
-    source: Path,
+    root: Path,
     progress: Progress = Ignore_Progress,
     platform: String = default_platform,
     options: List[String] = Nil,
     other_bash: String = "")
   {
-    source.is_dir || error("Bad source directory: " + source)
+    if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
+      error("Bad Poly/ML root directory: " + root)
 
     val info =
       platform_info.get(platform) getOrElse
@@ -87,7 +88,7 @@
 
     Isabelle_System.bash(
       if (other_bash == "") script else Bash.string(other_bash) + " -c " + Bash.string(script),
-      cwd = source.file, env = null,
+      cwd = root.file, env = null,
       progress_stdout = progress.echo(_),
       progress_stderr = progress.echo(_)).check
 
@@ -98,7 +99,7 @@
 
     for {
       d <- List("target/bin", "target/lib")
-      dir = source + Path.explode(d)
+      dir = root + Path.explode(d)
       entry <- File.read_dir(dir)
     } File.move(dir + Path.explode(entry), target)
 
@@ -113,34 +114,29 @@
     Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
     {
       Command_Line.tool0 {
-        var options = List.empty[String]
         var other_bash = ""
         var platform = default_platform
 
         val getopts = Getopts("""
-Usage: isabelle build_polyml [OPTIONS] [SOURCE]
+Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
 
   Options are:
-    -O OPTS...   additional options ./configure (e.g. --with-gmp)
     -b EXE       other bash executable (notably for msys on Windows)
-    -p PLATFORM  platform identifier and target directory
+    -p PLATFORM  platform identifier and target directory (default: """ + default_platform + """)
 
-  Build Poly/ML in SOURCE directory (default: .) for
-  given PLATFORM (default: """ + default_platform + """).
+  Build Poly/ML in its source ROOT directory of its sources, with additional
+  CONFIGURE_OPTIONS (e.g. --with-gmp).
 """,
-          "O:" -> (arg => options = options ::: List(arg)),
           "b:" -> (arg => other_bash = arg),
           "p:" -> (arg => platform = arg))
 
         val more_args = getopts(args)
-        val source =
+        val (root, options) =
           more_args match {
-            case Nil => Path.current
-            case List(source) => Path.explode(source)
-            case _ => getopts.usage()
+            case root :: options => (Path.explode(root), options)
+            case Nil => getopts.usage()
           }
-        build_polyml(source,
-          progress = new Console_Progress, platform = platform, options = options,
+        build_polyml(root, progress = new Console_Progress, platform = platform, options = options,
             other_bash = other_bash)
       }
     }, admin = true)