# HG changeset patch
# User wenzelm
# Date 1520796685 -3600
# Node ID 661cd25304ae3697e7ba756fee1a54807149a434
# Parent  92cf045c876bddbfbeb95c85e6954b590ba3661b
more compact markup tree: output messages are already stored in command results (e.g. relevant for  XML data representation);

diff -r 92cf045c876b -r 661cd25304ae src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Mar 11 15:28:22 2018 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 11 20:31:25 2018 +0100
@@ -162,6 +162,16 @@
 
   object State
   {
+    def get_result(states: List[State], serial: Long): Option[XML.Tree] =
+      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)
+
     def merge_results(states: List[State]): Results =
       Results.merge(states.map(_.results))
 
@@ -309,16 +319,16 @@
         case XML.Elem(Markup(name, props), body) =>
           props match {
             case Markup.Serial(i) =>
-              val message1 = XML.Elem(Markup(Markup.message(name), props), body)
-              val message2 = XML.Elem(Markup(name, props), body)
+              val markup_message = XML.Elem(Markup(Markup.message(name), props), body)
+              val message_markup = XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))
 
-              var st = copy(results = results + (i -> message1))
+              var st = copy(results = results + (i -> markup_message))
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
                   range <- Protocol_Message.positions(
                     self_id, command.span.position, chunk_name, chunk, message)
-                } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
+                } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup))
               }
               st
 
diff -r 92cf045c876b -r 661cd25304ae src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Mar 11 15:28:22 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Mar 11 20:31:25 2018 +0100
@@ -549,13 +549,17 @@
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   {
     val results =
-      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ =>
+      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
         {
           case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
 
-          case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
-          if Rendering.tooltip_message_elements(name) && body.nonEmpty =>
-            Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body)))
+          case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
+          if body.nonEmpty => Some(info + (r0, i, msg))
+
+          case (info, Text.Info(r0, XML.Elem(Markup(name, props), _)))
+          if Rendering.tooltip_message_elements(name) =>
+            for ((i, tree) <- Command.State.get_result_proper(command_states, props))
+            yield (info + (r0, i, tree))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
           if kind != "" && kind != Markup.ML_DEF =>
diff -r 92cf045c876b -r 661cd25304ae src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 11 15:28:22 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 11 20:31:25 2018 +0100
@@ -134,13 +134,17 @@
 
   def diagnostics: List[Text.Info[Command.Results]] =
     snapshot.cumulate[Command.Results](
-      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
-      {
-        case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
-        if body.nonEmpty => Some(res + (i -> msg))
+      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements,
+        command_states =>
+          {
+            case (res, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
+            if body.nonEmpty => Some(res + (i -> msg))
 
-        case _ => None
-      }).filterNot(info => info.info.is_empty)
+            case (res, Text.Info(_, msg)) =>
+              Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _)
+
+            case _ => None
+          }).filterNot(info => info.info.is_empty)
 
   def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
   {