# HG changeset patch
# User wenzelm
# Date 1497968274 -7200
# Node ID cdb6c10122b6f66d81418e74b12ac8ca50c96445
# Parent  6a8f8be2741c5ca64a4c7bc73a5d31e72417f5d5
tuned signature;

diff -r 6a8f8be2741c -r cdb6c10122b6 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Tue Jun 20 16:14:38 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Tue Jun 20 16:17:54 2017 +0200
@@ -331,7 +331,7 @@
     kind: Option[Int] = None,
     detail: Option[String] = None,
     documentation: Option[String] = None,
-    insertText: Option[String] = None,
+    text: Option[String] = None,
     range: Option[Line.Range] = None,
     command: Option[Command] = None)
   {
@@ -340,10 +340,10 @@
       JSON.optional("kind" -> kind) ++
       JSON.optional("detail" -> detail) ++
       JSON.optional("documentation" -> documentation) ++
-      JSON.optional("insertText" -> insertText) ++
+      JSON.optional("insertText" -> text) ++
       JSON.optional("range" -> range.map(Range(_))) ++
       JSON.optional("textEdit" ->
-        range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label)))) ++
+        range.map(r => Map("range" -> Range(r), "newText" -> text.getOrElse(label)))) ++
       JSON.optional("command" -> command.map(_.json))
   }
 
diff -r 6a8f8be2741c -r cdb6c10122b6 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 16:14:38 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 16:17:54 2017 +0200
@@ -224,7 +224,7 @@
         def item(command: Protocol.Command): Protocol.CompletionItem =
           Protocol.CompletionItem(
             label = command.title,
-            insertText = Some(""),
+            text = Some(""),
             range = Some(model.content.doc.range(Text.Range(caret))),
             command = Some(command))