# HG changeset patch
# User wenzelm
# Date 1754841635 -7200
# Node ID d25a6d2961214f1356167e9957c58458f4a7593f
# Parent  a28d9192d31eb7fe72da3041003c10f833192d7d
tuned signature: more explicit operations;

diff -r a28d9192d31e -r d25a6d296121 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sun Aug 10 15:17:13 2025 +0200
+++ b/src/Pure/Build/build.scala	Sun Aug 10 18:00:35 2025 +0200
@@ -795,6 +795,22 @@
 
   /* print messages */
 
+  def print_log_check(
+    pos: Position.T,
+    elem: XML.Elem,
+    message_head: List[Regex],
+    message_body: List[Regex]
+  ): Boolean = {
+    def check(filter: List[Regex], make_string: => String): Boolean =
+      filter.isEmpty || {
+        val s = Protocol_Message.clean_output(make_string)
+        filter.forall(r => r.findFirstIn(Protocol_Message.clean_output(s)).nonEmpty)
+      }
+
+    check(message_head, Protocol.message_heading(elem, pos)) &&
+    check(message_body, Pretty.unformatted_string_of(List(elem)))
+  }
+
   def print_log(
     options: Options,
     sessions: List[String],
@@ -810,12 +826,6 @@
     val session = Session.bootstrap(options)
     val store = session.store
 
-    def check(filter: List[Regex], make_string: => String): Boolean =
-      filter.isEmpty || {
-        val s = Protocol_Message.clean_output(make_string)
-        filter.forall(r => r.findFirstIn(Protocol_Message.clean_output(s)).nonEmpty)
-      }
-
     def print(session_name: String): Unit = {
       using(Export.open_session_context0(store, session_name)) { session_context =>
         val result =
@@ -850,13 +860,11 @@
                     for (Text.Info(range, elem) <- messages) {
                       val line = line_document.position(range.start).line1
                       val pos = Position.Line_File(line, snapshot.node_name.node)
-                      def message_text: String =
-                        Protocol.message_text(elem, heading = true, pos = pos,
-                          margin = margin, breakgain = breakgain, metric = metric)
-                      val ok =
-                        check(message_head, Protocol.message_heading(elem, pos)) &&
-                        check(message_body, Pretty.unformatted_string_of(List(elem)))
-                      if (ok) buffer += message_text
+                      if (print_log_check(pos, elem, message_head, message_body)) {
+                        buffer +=
+                          Protocol.message_text(elem, heading = true, pos = pos,
+                            margin = margin, breakgain = breakgain, metric = metric)
+                      }
                     }
                     if (buffer.nonEmpty) {
                       progress.echo(thy_heading)