# HG changeset patch
# User wenzelm
# Date 1488657884 -3600
# Node ID a57794dbe0af5e7d64a597fb5b84c1a885274398
# Parent  1f47b92021debbd211a7d7519a0f12c2250ca447
more general hover_message (see also JEdit_Rendering.tooltip_message);

diff -r 1f47b92021de -r a57794dbe0af src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Sat Mar 04 20:26:32 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sat Mar 04 21:04:44 2017 +0100
@@ -61,7 +61,7 @@
   for (let color of foreground_colors) {
     types["foreground_".concat(color)] = background(color) // approximation
   }
-  types["bad"] = decoration({})
+  types["hover_message"] = decoration({})
 }
 
 
diff -r 1f47b92021de -r a57794dbe0af src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Sat Mar 04 20:26:32 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Sat Mar 04 21:04:44 2017 +0100
@@ -417,11 +417,6 @@
 
   /* decorations */
 
-  object Decorations
-  {
-    val bad = "bad"
-  }
-
   sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
   {
     def no_hover_message: Boolean = hover_message.isEmpty
diff -r 1f47b92021de -r a57794dbe0af src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Mar 04 20:26:32 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Mar 04 21:04:44 2017 +0100
@@ -46,7 +46,7 @@
   private val diagnostics_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
 
-  private val bad_elements = Markup.Elements(Markup.BAD)
+  private val hover_message_elements = Markup.Elements(Markup.BAD)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
@@ -111,23 +111,32 @@
 
   /* decorations */
 
+  def hover_message: Document_Model.Decoration =
+  {
+    val results =
+      snapshot.cumulate[Command.Results](
+        model.content.text_range, Command.Results.empty,
+        VSCode_Rendering.hover_message_elements, _ =>
+          {
+            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+            if body.nonEmpty =>
+              Some(msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body)))
+
+            case _ => None
+          })
+    val content =
+      for (Text.Info(r, msgs) <- results if !msgs.is_empty)
+      yield Text.Info(r, (for ((_, t) <- msgs.iterator) yield List(t)).toList)
+    Document_Model.Decoration("hover_message", content)
+  }
+
   def decorations: List[Document_Model.Decoration] =
-    decorations_bad :::
+    hover_message ::
     VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
       background(model.content.text_range, Set.empty)) :::
     VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
       foreground(model.content.text_range))
 
-  def decorations_bad: List[Document_Model.Decoration] =
-  {
-    val content =
-      snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
-        {
-          case Text.Info(_, XML.Elem(_, body)) => Some(List(body))
-        })
-    List(Document_Model.Decoration(Protocol.Decorations.bad, content))
-  }
-
   def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
   {
     val content =