src/Pure/Admin/build_history.scala

--- a/src/Pure/Admin/build_history.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -7,8 +7,7 @@
 package isabelle
 
 
-object Build_History
-{
+object Build_History {
   /* log files */
 
   val engine = "build_history"
@@ -23,10 +22,9 @@
     arch_64: Boolean,
     heap: Int,
     max_heap: Option[Int],
-    more_settings: List[String]): String =
-  {
-    val (ml_platform, ml_settings) =
-    {
+    more_settings: List[String]
+  ): String = {
+    val (ml_platform, ml_settings) = {
       val cygwin_32 = "x86-cygwin"
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
@@ -123,8 +121,8 @@
     more_preferences: List[String] = Nil,
     verbose: Boolean = false,
     build_tags: List[String] = Nil,
-    build_args: List[String] = Nil): List[(Process_Result, Path)] =
-  {
+    build_args: List[String] = Nil
+  ): List[(Process_Result, Path)] = {
     /* sanity checks */
 
     if (File.eq(Path.ISABELLE_HOME, root))
@@ -148,8 +146,7 @@
 
     /* checkout Isabelle + AFP repository */
 
-    def checkout(dir: Path, version: String): String =
-    {
+    def checkout(dir: Path, version: String): String = {
       val hg = Mercurial.repository(dir)
       hg.update(rev = version, clean = true)
       progress.echo_if(verbose, hg.log(version, options = "-l1"))
@@ -188,8 +185,7 @@
     val build_group_id = build_host + ":" + build_history_date.time.ms
 
     var first_build = true
-    for ((threads, processes) <- multicore_list) yield
-    {
+    for ((threads, processes) <- multicore_list) yield {
       /* init settings */
 
       val component_settings =
@@ -285,13 +281,11 @@
 
       build_out_progress.echo("Reading session build info ...")
       val session_build_info =
-        build_info.finished_sessions.flatMap(session_name =>
-          {
+        build_info.finished_sessions.flatMap(session_name => {
             val database = isabelle_output + store.database(session_name)
 
             if (database.is_file) {
-              using(SQLite.open_database(database))(db =>
-              {
+              using(SQLite.open_database(database))(db => {
                 val theory_timings =
                   try {
                     store.read_theory_timings(db, session_name).map(ps =>
@@ -314,8 +308,7 @@
 
       build_out_progress.echo("Reading ML statistics ...")
       val ml_statistics =
-        build_info.finished_sessions.flatMap(session_name =>
-          {
+        build_info.finished_sessions.flatMap(session_name => {
             val database = isabelle_output + store.database(session_name)
             val log_gz = isabelle_output + store.log_gz(session_name)
 
@@ -342,8 +335,7 @@
 
       build_out_progress.echo("Reading error messages ...")
       val session_errors =
-        build_info.failed_sessions.flatMap(session_name =>
-          {
+        build_info.failed_sessions.flatMap(session_name => {
             val database = isabelle_output + store.database(session_name)
             val errors =
               if (database.is_file) {
@@ -358,8 +350,7 @@
 
       build_out_progress.echo("Reading heap sizes ...")
       val heap_sizes =
-        build_info.finished_sessions.flatMap(session_name =>
-          {
+        build_info.finished_sessions.flatMap(session_name => {
             val heap = isabelle_output + Path.explode(session_name)
             if (heap.is_file)
               Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
@@ -392,8 +383,7 @@
 
   /* command line entry point */
 
-  private object Multicore
-  {
+  private object Multicore {
     private val Pat1 = """^(\d+)$""".r
     private val Pat2 = """^(\d+)x(\d+)$""".r
 
@@ -405,8 +395,7 @@
       }
   }
 
-  def main(args: Array[String]): Unit =
-  {
+  def main(args: Array[String]): Unit = {
     Command_Line.tool {
       var afp_rev: Option[String] = None
       var multicore_base = false
@@ -546,8 +535,8 @@
     rev: String = "",
     afp_rev: Option[String] = None,
     options: String = "",
-    args: String = ""): List[(String, Bytes)] =
-  {
+    args: String = ""
+  ): List[(String, Bytes)] = {
     /* Isabelle self repository */
 
     val self_hg =
@@ -594,8 +583,7 @@
 
     /* Admin/build_history */
 
-    ssh.with_tmp_dir(tmp_dir =>
-    {
+    ssh.with_tmp_dir(tmp_dir => {
       val output_file = tmp_dir + Path.explode("output")
 
       val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)