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)