# HG changeset patch
# User wenzelm
# Date 1607616119 -3600
# Node ID 530534f2f0fd9428ae4be522b20e00a7c9923402
# Parent  17533d0a11b8c8344344a941a5af9b3b0e28386f
clarified types;

diff -r 17533d0a11b8 -r 530534f2f0fd src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Thu Dec 10 17:01:14 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Thu Dec 10 17:01:59 2020 +0100
@@ -543,32 +543,25 @@
   def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] =
   {
     val results =
-      snapshot.cumulate[Vector[XML.Elem]](range, Vector.empty, Rendering.message_elements,
-        states =>
+      snapshot.cumulate[Vector[Command.Results.Entry]](
+        range, Vector.empty, Rendering.message_elements, command_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
-              }
+              Command.State.get_result_proper(command_states, elem.markup.properties)
+                .map(res :+ _)
             case _ => None
           })
 
     var seen_serials = Set.empty[Long]
-    def seen(elem: XML.Elem): Boolean =
-      elem.markup.properties match {
-        case Markup.Serial(i) => val b = seen_serials(i); seen_serials += i; b
-        case _ => false
-      }
+    def seen(i: Long): Boolean =
+    {
+      val b = seen_serials(i)
+      seen_serials += i
+      b
+    }
     for {
-      Text.Info(range, elems) <- results
-      elem <- elems
-      if !seen(elem)
+      Text.Info(range, entries) <- results
+      (i, elem) <- entries if !seen(i)
     } yield Text.Info(range, elem)
   }