diff -r d5773922358d -r eb44cf7ae926 src/Pure/Admin/build_polyml.scala --- a/src/Pure/Admin/build_polyml.scala Sat Apr 04 19:18:19 2020 +0200 +++ b/src/Pure/Admin/build_polyml.scala Sat Apr 04 19:30:45 2020 +0200 @@ -256,12 +256,11 @@ val isabelle_tool1 = Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => { - Command_Line.tool { - var msys_root: Option[Path] = None - var arch_64 = false - var sha1_root: Option[Path] = None + var msys_root: Option[Path] = None + 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: @@ -272,33 +271,31 @@ Build Poly/ML in the ROOT directory of its sources, with additional CONFIGURE_OPTIONS (e.g. --without-gmp). """, - "M:" -> (arg => msys_root = Some(Path.explode(arg))), - "m:" -> - { - case "32" | "x86_64_32" => 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)))) + "M:" -> (arg => msys_root = Some(Path.explode(arg))), + "m:" -> + { + case "32" | "x86_64_32" => 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, msys_root = msys_root) - } + 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, msys_root = msys_root) }) val isabelle_tool2 = Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args => { - Command_Line.tool { - var sha1_root: Option[Path] = None + var sha1_root: Option[Path] = None - val getopts = Getopts(""" + val getopts = Getopts(""" Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR Options are: @@ -307,16 +304,15 @@ Make skeleton for Poly/ML component, based on official source archive (zip or tar.gz). """, - "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) + "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) - val more_args = getopts(args) + val more_args = getopts(args) - val (source_archive, component_dir) = - more_args match { - case List(archive, dir) => (Path.explode(archive), Path.explode(dir)) - case _ => getopts.usage() - } - build_polyml_component(source_archive, component_dir, sha1_root = sha1_root) - } + val (source_archive, component_dir) = + more_args match { + case List(archive, dir) => (Path.explode(archive), Path.explode(dir)) + case _ => getopts.usage() + } + build_polyml_component(source_archive, component_dir, sha1_root = sha1_root) }) }