# HG changeset patch # User wenzelm # Date 1687947226 -7200 # Node ID 60fa7a0b9372daf0a70d66aa7683e0664f34d142 # Parent 82efaf1bf3c75845948bf3e4da139240171992d6 clarified output; diff -r 82efaf1bf3c7 -r 60fa7a0b9372 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Jun 28 11:44:09 2023 +0200 +++ b/src/Pure/Tools/build.scala Wed Jun 28 12:13:46 2023 +0200 @@ -385,21 +385,36 @@ using_option(Store(options).maybe_open_build_database(Build_Process.Data.database))( Build_Process.read_builds).getOrElse(Nil) - def print_builds(builds: List[Build_Process.Build]): String = - if (builds.isEmpty) "No build processes available" - else { - "Available build processes:" + - (for ((build, i) <- builds.iterator.zipWithIndex) - yield "\n " + (i + 1) + ": " + build.build_uuid).mkString + def print_builds(options: Options, builds: List[Build_Process.Build]): String = + using_optional(Store(options).maybe_open_build_database(Build_Process.Data.database)) { build_database => + val print_database = + build_database match { + case None => "" + case Some(db) => " (database " + db + ")" + } + if (builds.isEmpty) "No build processes available" + print_database + else { + "Available build processes" + print_database + ":" + + (for ((build, i) <- builds.iterator.zipWithIndex) + yield { + "\n " + (i + 1) + ": " + build.build_uuid + + " (platform: " + build.ml_platform + + ", start: " + Build_Log.print_date(build.start) + ")" + }).mkString + } } - def id_builds(id: String, builds: List[Build_Process.Build]): Build_Process.Build = + def id_builds( + options: Options, + id: String, + builds: List[Build_Process.Build] + ): Build_Process.Build = (id, builds.length) match { case (Value.Int(i), n) if 1 <= i && i <= n => builds(i - 1) case (UUID(_), _) if builds.exists(_.build_uuid == id) => builds.find(_.build_uuid == id).get - case ("", 0) => error(print_builds(builds)) + case ("", 0) => error(print_builds(options, builds)) case ("", 1) => builds.head - case _ => cat_error("Cannot identify build process " + quote(id), print_builds(builds)) + case _ => cat_error("Cannot identify build process " + quote(id), print_builds(options, builds)) } @@ -484,10 +499,10 @@ val builds = read_builds(options) - if (list_builds) progress.echo(print_builds(builds)) + if (list_builds) progress.echo(print_builds(options, builds)) if (!list_builds || build_id.nonEmpty) { - val build = id_builds(build_id, builds) + val build = id_builds(options, build_id, builds) val results = progress.interrupt_handler {