# HG changeset patch
# User wenzelm
# Date 1488655592 -3600
# Node ID 1f47b92021debbd211a7d7519a0f12c2250ca447
# Parent  66b19d05dcee4175af2ed2df156e77abf9a5dfb8
clarified signature;

diff -r 66b19d05dcee -r 1f47b92021de src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Mar 04 13:36:06 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Mar 04 20:26:32 2017 +0100
@@ -16,7 +16,7 @@
 {
   /* decorations */
 
-  sealed case class Decoration(typ: String, content: List[Text.Info[XML.Body]])
+  sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]])
 
 
   /* content */
diff -r 66b19d05dcee -r 1f47b92021de src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Mar 04 13:36:06 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Mar 04 20:26:32 2017 +0100
@@ -17,20 +17,16 @@
 {
   /* decorations */
 
-  def color_decorations(prefix: String, types: Rendering.Color.ValueSet,
+  private def color_decorations(prefix: String, types: Rendering.Color.ValueSet,
     colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
   {
     val color_ranges =
       (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
         case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
       }
-    for (c <- types.toList)
-    yield {
-      val typ = prefix + c.toString
-      val content =
-        color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: XML.Body))
-      Document_Model.Decoration(typ, content)
-    }
+    types.toList.map(c =>
+      Document_Model.Decoration(prefix + c.toString,
+        color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: List[XML.Body]))))
   }
 
 
@@ -127,7 +123,7 @@
     val content =
       snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
         {
-          case Text.Info(_, XML.Elem(_, body)) => Some(body)
+          case Text.Info(_, XML.Elem(_, body)) => Some(List(body))
         })
     List(Document_Model.Decoration(Protocol.Decorations.bad, content))
   }
@@ -135,11 +131,12 @@
   def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
   {
     val content =
-      for (Text.Info(text_range, body) <- decoration.content)
+      for (Text.Info(text_range, msgs) <- decoration.content)
       yield {
         val range = model.content.doc.range(text_range)
-        val msg = resources.output_pretty(body, diagnostics_margin)
-        Protocol.DecorationOptions(range, if (msg == "") Nil else List(Protocol.MarkedString(msg)))
+        Protocol.DecorationOptions(range,
+          msgs.map(msg =>
+            Protocol.MarkedString(resources.output_pretty(msg, diagnostics_margin))))
       }
     Protocol.Decoration(decoration.typ, content)
   }