# HG changeset patch
# User wenzelm
# Date 1753811944 -7200
# Node ID 1337812b6d10e3e0920d66f10236a1deb123e873
# Parent  fa8067dc67876a8ed1d0c4983b2fef1e2f532300
clarified signature;

diff -r fa8067dc6787 -r 1337812b6d10 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Tue Jul 29 17:01:57 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Jul 29 19:59:04 2025 +0200
@@ -818,9 +818,8 @@
               Build.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
                 case None => progress.echo(thy_heading + " MISSING")
                 case Some(snapshot) =>
-                  val rendering = new Rendering(snapshot, options, session)
                   val messages =
-                    rendering.text_messages()
+                    Rendering.text_messages(snapshot)
                       .filter(message => progress.verbose || Protocol.is_exported(message.info))
                   if (messages.nonEmpty) {
                     val line_document = Line.Document(snapshot.node.source)
diff -r fa8067dc6787 -r 1337812b6d10 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Jul 29 17:01:57 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Jul 29 19:59:04 2025 +0200
@@ -96,6 +96,34 @@
     error_pri -> Color.error_message)
 
 
+  /* text messages */
+
+  def text_messages(
+    snapshot: Document.Snapshot,
+    range: Text.Range = Text.Range.full
+  ): List[Text.Info[XML.Elem]] = {
+    val results =
+      snapshot.cumulate[Vector[Command.Results.Entry]](
+        range, Vector.empty, message_elements, command_states =>
+          {
+            case (res, Text.Info(_, elem)) =>
+              Command.State.get_result_proper(command_states, elem.markup.properties)
+                .map(res :+ _)
+          })
+
+    var seen_serials = Set.empty[Long]
+    def seen(i: Long): Boolean = {
+      val b = seen_serials(i)
+      seen_serials += i
+      b
+    }
+    for {
+      Text.Info(range, entries) <- results
+      (i, elem) <- entries if !seen(i)
+    } yield Text.Info(range, elem)
+  }
+
+
   /* text color */
 
   def get_text_color(markup: Markup): Option[Color.Value] =
@@ -561,28 +589,6 @@
     } yield Text.Info(r, color)
   }
 
-  def text_messages(range: Text.Range = Text.Range.full): List[Text.Info[XML.Elem]] = {
-    val results =
-      snapshot.cumulate[Vector[Command.Results.Entry]](
-        range, Vector.empty, Rendering.message_elements, command_states =>
-          {
-            case (res, Text.Info(_, elem)) =>
-              Command.State.get_result_proper(command_states, elem.markup.properties)
-                .map(res :+ _)
-          })
-
-    var seen_serials = Set.empty[Long]
-    def seen(i: Long): Boolean = {
-      val b = seen_serials(i)
-      seen_serials += i
-      b
-    }
-    for {
-      Text.Info(range, entries) <- results
-      (i, elem) <- entries if !seen(i)
-    } yield Text.Info(range, elem)
-  }
-
 
   /* markup structure */