tuned output;
authorFabian Huch <huch@in.tum.de>
Sat, 01 Feb 2025 22:20:42 +0100
changeset 82039 e0ba5e9850df
parent 82038 42fe486d38d5
child 82040 0dc7b3253aaa
tuned output;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Sat Feb 01 20:46:01 2025 +0100
+++ b/src/Pure/Build/build_manager.scala	Sat Feb 01 22:20:42 2025 +0100
@@ -1704,17 +1704,6 @@
 
   /* Isabelle tool wrapper */
 
-  private def show_options(relevant_options: List[String], options: Options): String =
-    cat_lines(relevant_options.flatMap(options.get).map(_.print))
-
-  private val notable_server_options =
-    List(
-      "build_manager_dir",
-      "build_manager_address",
-      "build_manager_ssh_host",
-      "build_manager_ssh_group",
-      "build_manager_ci_jobs")
-
   val isabelle_tool = Isabelle_Tool("build_manager", "run build manager", Scala_Project.here,
     { args =>
       var afp_root: Option[Path] = None
@@ -1734,9 +1723,8 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p PORT      explicit web server port
 
-  Run Isabelle build manager. Notable system options:
-
-""" + Library.indent_lines(2, show_options(notable_server_options, options)) + "\n",
+  Run Isabelle build manager.
+""",
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "D:" -> (arg => dirs += Path.explode(arg)),
         "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.global, arg)),
@@ -1934,8 +1922,6 @@
 
   /* Isabelle tool wrapper */
 
-  val notable_client_options = List("build_manager_ssh_user", "build_manager_ssh_group")
-
   val isabelle_tool2 = Isabelle_Tool("build_task", "submit build task for build manager",
     Scala_Project.here,
     { args =>
@@ -1979,7 +1965,7 @@
 
   Submit build task on SSH server. Notable system options:
 
-""" + Library.indent_lines(2, show_options(notable_client_options, options)) + "\n",
+""" + Library.indent_lines(2, options.get("build_manager_ssh_user").get.print) + "\n",
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "B:" -> (arg => base_sessions += arg),
         "P" -> (_ => presentation = true),