--- 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 =