src/Pure/PIDE/rendering.scala

--- a/src/Pure/PIDE/rendering.scala	Wed Dec 09 15:53:45 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 09 20:10:10 2020 +0100
@@ -211,6 +211,7 @@
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
       Markup.BAD)
 
+  val message_elements = Markup.Elements(message_pri.keySet)
   val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
   val error_elements = Markup.Elements(Markup.ERROR)
 
@@ -520,7 +521,7 @@
   }
 
 
-  /* message underline color */
+  /* messages */
 
   def message_underline_color(elements: Markup.Elements, range: Text.Range)
     : List[Text.Info[Rendering.Color.Value]] =
@@ -536,6 +537,39 @@
     } yield Text.Info(r, color)
   }
 
+  def text_messages(range: Text.Range): List[Text.Info[XML.Tree]] =
+  {
+    val results =
+      snapshot.cumulate[Vector[XML.Tree]](range, Vector.empty, Rendering.message_elements,
+        states =>
+          {
+            case (res, Text.Info(_, elem)) =>
+              elem.markup.properties match {
+                case Markup.Serial(i) =>
+                  states.collectFirst(
+                  {
+                    case st if st.results.get(i).isDefined =>
+                      res :+ st.results.get(i).get
+                  })
+                case _ => None
+              }
+            case _ => None
+          })
+
+    var seen_serials = Set.empty[Long]
+    val seen: XML.Tree => Boolean =
+    {
+      case XML.Elem(Markup(_, Markup.Serial(i)), _) =>
+        val b = seen_serials(i); seen_serials += i; b
+      case _ => false
+    }
+    for {
+      Text.Info(range, trees) <- results
+      tree <- trees
+      if !seen(tree)
+    } yield Text.Info(range, tree)
+  }
+
 
   /* tooltips */