--- a/src/Tools/VSCode/src/protocol.scala Sat Jun 10 21:34:05 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala Sat Jun 10 21:48:02 2017 +0200
@@ -326,12 +326,12 @@
range: Option[Line.Range] = None)
{
def json: JSON.T =
- Message.empty + ("label" -> label) ++
- JSON.optional("kind" -> kind) ++
- JSON.optional("detail" -> detail) ++
- JSON.optional("documentation" -> documentation) ++
- JSON.optional("insertText" -> insertText) ++
- JSON.optional("range" -> range.map(Range(_)))
+ Map("label" -> label) ++
+ JSON.optional("kind" -> kind) ++
+ JSON.optional("detail" -> detail) ++
+ JSON.optional("documentation" -> documentation) ++
+ JSON.optional("insertText" -> insertText) ++
+ JSON.optional("range" -> range.map(Range(_)))
}
object Completion extends RequestTextDocumentPosition("textDocument/completion")