--- 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)
})
}
--- a/src/Pure/Tools/profiling_report.scala Sat Apr 04 19:18:19 2020 +0200
+++ b/src/Pure/Tools/profiling_report.scala Sat Apr 04 19:30:45 2020 +0200
@@ -32,24 +32,22 @@
val isabelle_tool =
Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args =>
{
- Command_Line.tool {
- val getopts =
- Getopts("""
+ val getopts =
+ Getopts("""
Usage: isabelle profiling_report [LOGS ...]
Report Poly/ML profiling output from log files (potentially compressed).
""")
- val log_names = getopts(args)
- for (name <- log_names) {
- val log_file = Build_Log.Log_File(Path.explode(name))
- val results =
- for ((count, fun) <- profiling_report(log_file))
- yield
- String.format(Locale.ROOT, "%14d %s",
- count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef])
- if (results.nonEmpty)
- Output.writeln(cat_lines((log_file.name + ":") :: results))
- }
+ val log_names = getopts(args)
+ for (name <- log_names) {
+ val log_file = Build_Log.Log_File(Path.explode(name))
+ val results =
+ for ((count, fun) <- profiling_report(log_file))
+ yield
+ String.format(Locale.ROOT, "%14d %s",
+ count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef])
+ if (results.nonEmpty)
+ Output.writeln(cat_lines((log_file.name + ":") :: results))
}
})
}