# HG changeset patch
# User wenzelm
# Date 1497127715 -7200
# Node ID 175772371cd015b8d22cfb11b6ba1f7c88e2db8c
# Parent  880db47fed30d5c2513ef6399d5ce87c8e864349
use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);

diff -r 880db47fed30 -r 175772371cd0 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Sat Jun 10 21:48:02 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Sat Jun 10 22:48:35 2017 +0200
@@ -331,7 +331,9 @@
       JSON.optional("detail" -> detail) ++
       JSON.optional("documentation" -> documentation) ++
       JSON.optional("insertText" -> insertText) ++
-      JSON.optional("range" -> range.map(Range(_)))
+      JSON.optional("range" -> range.map(Range(_))) ++
+      JSON.optional("textEdit" ->
+        range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label))))
   }
 
   object Completion extends RequestTextDocumentPosition("textDocument/completion")