# HG changeset patch
# User wenzelm
# Date 1488894712 -3600
# Node ID 1191df79aa1cc7d18cfce209641da007fcc7f3e1
# Parent  0a2c0712e4326eab1e3e151ef68c15ea01b71bc6
tuned signature;

diff -r 0a2c0712e432 -r 1191df79aa1c src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Tue Mar 07 14:33:14 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Tue Mar 07 14:51:52 2017 +0100
@@ -16,6 +16,13 @@
 {
   /* decorations */
 
+  object Decoration
+  {
+    def empty(typ: String): Decoration = Decoration(typ, Nil)
+
+    def ranges(typ: String, ranges: List[Text.Range]): Decoration =
+      Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body])))
+  }
   sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]])
 
 
@@ -127,7 +134,7 @@
     val diagnostics = rendering.diagnostics
     val decorations =
       if (node_visible) rendering.decorations
-      else { for (deco <- published_decorations) yield Document_Model.Decoration(deco.typ, Nil) }
+      else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) }
 
     val changed_diagnostics =
       if (diagnostics == published_diagnostics) None else Some(diagnostics)
diff -r 0a2c0712e432 -r 1191df79aa1c src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 14:33:14 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 14:51:52 2017 +0100
@@ -25,8 +25,7 @@
         case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
       }
     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]))))
+      Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
   }
 
   private val dotted_colors =