tuned -- Command_Line.tool is already part of Isabelle_Tool;
authorwenzelm
Sat, 04 Apr 2020 19:30:45 +0200
changeset 71686 eb44cf7ae926
parent 71685 d5773922358d
child 71687 f17be1db8381
tuned -- Command_Line.tool is already part of Isabelle_Tool;
src/Pure/Admin/build_polyml.scala
src/Pure/Tools/profiling_report.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)
     })
 }
--- 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))
       }
     })
 }