src/Tools/VSCode/src/vscode_rendering.scala
changeset 65173 3700be571a01
parent 65146 69ea3f1715be
child 65174 c0388fbd8096
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 14:16:45 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 16:07:20 2017 +0100
@@ -162,7 +162,7 @@
       for (Text.Info(text_range, msgs) <- decoration.content)
       yield {
         val range = model.content.doc.range(text_range)
-        Protocol.DecorationOptions(range,
+        Protocol.DecorationOpts(range,
           msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
       }
     Protocol.Decoration(decoration.typ, content)