clarified signature: more specific types;

--- a/src/Pure/PIDE/command.scala	Thu Dec 10 15:27:41 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Dec 10 16:35:56 2020 +0100
@@ -54,17 +54,17 @@
 
   object Results
   {
-    type Entry = (Long, XML.Tree)
+    type Entry = (Long, XML.Elem)
     val empty: Results = new Results(SortedMap.empty)
     def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
     def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
   }
 
-  final class Results private(private val rep: SortedMap[Long, XML.Tree])
+  final class Results private(private val rep: SortedMap[Long, XML.Elem])
   {
     def is_empty: Boolean = rep.isEmpty
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
-    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
+    def get(serial: Long): Option[XML.Elem] = rep.get(serial)
     def iterator: Iterator[Results.Entry] = rep.iterator
 
     def + (entry: Results.Entry): Results =
@@ -187,15 +187,15 @@
 
   object State
   {
-    def get_result(states: List[State], serial: Long): Option[XML.Tree] =
+    def get_result(states: List[State], serial: Long): Option[XML.Elem] =
       states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get)
 
     def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] =
       for {
         serial <- Markup.Serial.unapply(props)
-        tree @ XML.Elem(_, body) <- get_result(states, serial)
-        if body.nonEmpty
-      } yield (serial -> tree)
+        elem <- get_result(states, serial)
+        if elem.body.nonEmpty
+      } yield serial -> elem
 
     def merge_results(states: List[State]): Results =
       Results.merge(states.map(_.results))

--- a/src/Pure/PIDE/document.scala	Thu Dec 10 15:27:41 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Dec 10 16:35:56 2020 +0100
@@ -637,14 +637,14 @@
 
     /* messages */
 
-    lazy val messages: List[(XML.Tree, Position.T)] =
+    lazy val messages: List[(XML.Elem, Position.T)] =
       (for {
         (command, start) <-
           Document.Node.Commands.starts_pos(
             node.commands.iterator, Token.Pos.file(node_name.node))
         pos = command.span.keyword_pos(start).position(command.span.name)
-        (_, tree) <- state.command_results(version, command).iterator
-       } yield (tree, pos)).toList
+        (_, elem) <- state.command_results(version, command).iterator
+       } yield (elem, pos)).toList
 
 
     /* exports */

--- a/src/Pure/PIDE/rendering.scala	Thu Dec 10 15:27:41 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Thu Dec 10 16:35:56 2020 +0100
@@ -11,6 +11,9 @@
 import java.io.{File => JFile}
 import java.nio.file.FileSystems
 
+import scala.collection.immutable.SortedMap
+
+
 
 object Rendering
 {
@@ -94,7 +97,7 @@
     legacy_pri -> Color.legacy_message,
     error_pri -> Color.error_message)
 
-  def output_messages(results: Command.Results): List[XML.Tree] =
+  def output_messages(results: Command.Results): List[XML.Elem] =
   {
     val (states, other) =
       results.iterator.map(_._2).filterNot(Protocol.is_result).toList
@@ -537,10 +540,10 @@
     } yield Text.Info(r, color)
   }
 
-  def text_messages(range: Text.Range): List[Text.Info[XML.Tree]] =
+  def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] =
   {
     val results =
-      snapshot.cumulate[Vector[XML.Tree]](range, Vector.empty, Rendering.message_elements,
+      snapshot.cumulate[Vector[XML.Elem]](range, Vector.empty, Rendering.message_elements,
         states =>
           {
             case (res, Text.Info(_, elem)) =>
@@ -557,17 +560,16 @@
           })
 
     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
-    }
+    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
+      }
     for {
-      Text.Info(range, trees) <- results
-      tree <- trees
-      if !seen(tree)
-    } yield Text.Info(range, tree)
+      Text.Info(range, elems) <- results
+      elem <- elems
+      if !seen(elem)
+    } yield Text.Info(range, elem)
   }
 
 
@@ -578,7 +580,7 @@
   private sealed case class Tooltip_Info(
     range: Text.Range,
     timing: Timing = Timing.zero,
-    messages: List[Command.Results.Entry] = Nil,
+    messages: List[(Long, XML.Tree)] = Nil,
     rev_infos: List[(Boolean, XML.Tree)] = Nil)
   {
     def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
@@ -688,7 +690,8 @@
     else {
       val r = Text.Range(results.head.range.start, results.last.range.stop)
       val all_tips =
-        Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
+        (SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _)
+          .iterator.map(_._2).toList :::
         results.flatMap(res => res.infos(true)) :::
         results.flatMap(res => res.infos(false)).lastOption.toList
       if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))

--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 15:27:41 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 16:35:56 2020 +0100
@@ -36,9 +36,9 @@
         val results =
           Command.Results.make(
             for {
-              tree @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES)
+              elem @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES)
               i <- Markup.Serial.unapply(markup.properties)
-            } yield i -> tree)
+            } yield i -> elem)
 
         val blobs =
           blobs_files.map(file =>

--- a/src/Pure/Tools/dump.scala	Thu Dec 10 15:27:41 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Dec 10 16:35:56 2020 +0100
@@ -327,10 +327,10 @@
                 }
                 else {
                   val msgs =
-                    for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
+                    for ((elem, pos) <- snapshot.messages if Protocol.is_error(elem))
                     yield {
                       "Error" + Position.here(pos) + ":\n" +
-                        XML.content(Pretty.formatted(List(tree)))
+                        XML.content(Pretty.formatted(List(elem)))
                     }
                   progress.echo("FAILED to process theory " + name)
                   msgs.foreach(progress.echo_error_message)