# HG changeset patch
# User wenzelm
# Date 1497124082 -7200
# Node ID 880db47fed30d5c2513ef6399d5ce87c8e864349
# Parent  b2bfbefd354f749c12fe7a21f473ec9bc13b28f9
tuned;

diff -r b2bfbefd354f -r 880db47fed30 src/Tools/VSCode/src/protocol.scala
--- 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")