# HG changeset patch
# User wenzelm
# Date 1708603062 -3600
# Node ID 3f307faf9111e948404e58e4e6a8173fe15d1747
# Parent  d298c5b65d8efd239bb68971406b1181b003c746
tuned whitespace;

diff -r d298c5b65d8e -r 3f307faf9111 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Thu Feb 22 12:53:07 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Thu Feb 22 12:57:42 2024 +0100
@@ -277,7 +277,8 @@
               for {
                 elapsed <- Markup.Elapsed.unapply(props)
                 elapsed_time = Time.seconds(elapsed)
-                if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
+                if elapsed_time.is_relevant &&
+                   elapsed_time >= options.seconds("command_timing_threshold")
               } command_timings += props.filter(Markup.command_timing_property)
           }
 
@@ -292,7 +293,8 @@
                   if (!progress.stopped) {
                     val theory_name = snapshot.node_name.theory
                     val args =
-                      Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
+                      Protocol.Export.Args(
+                        theory_name = theory_name, name = name, compress = compress)
                     val body = Bytes(Symbol.encode(YXML.string_of_body(xml)))
                     export_consumer.make_entry(session_name, args, body)
                   }
@@ -401,8 +403,9 @@
                           output_sources = info.document_output,
                           output_pdf = info.document_output)
                     }
-                  using(database_context.open_database(session_name, output = true))(session_database =>
-                    documents.foreach(_.write(session_database.db, session_name)))
+                  using(database_context.open_database(session_name, output = true))(
+                    session_database =>
+                      documents.foreach(_.write(session_database.db, session_name)))
                   (documents.flatMap(_.log_lines), Nil)
                 }
               }
@@ -450,7 +453,9 @@
                     errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                       errs.map(Protocol.Error_Message_Marker.apply))
                 }
-                else if (progress.stopped && result1.ok) result1.copy(rc = Process_Result.RC.interrupt)
+                else if (progress.stopped && result1.ok) {
+                  result1.copy(rc = Process_Result.RC.interrupt)
+                }
                 else result1
               case Exn.Exn(Exn.Interrupt()) =>
                 if (result1.ok) result1.copy(rc = Process_Result.RC.interrupt)
@@ -538,11 +543,14 @@
           }
           else {
             progress.echo(
-              session_name + " FAILED (see also \"isabelle build_log -H Error " + session_name + "\")")
+              session_name + " FAILED (see also \"isabelle build_log -H Error " +
+              session_name + "\")")
             if (!process_result.interrupted) {
               val tail = info.options.int("process_output_tail")
-              val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)
-              val prefix = if (log_lines.length == suffix.length) Nil else List("...")
+              val suffix =
+                if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)
+              val prefix =
+                if (log_lines.length == suffix.length) Nil else List("...")
               progress.echo(Library.trim_line(cat_lines(prefix ::: suffix)))
             }
           }