src/Tools/VSCode/src/protocol.scala
changeset 66062 175772371cd0
parent 66061 880db47fed30
child 66090 5e1c1b366ac3
equal deleted inserted replaced
66061:880db47fed30 66062:175772371cd0
   329       Map("label" -> label) ++
   329       Map("label" -> label) ++
   330       JSON.optional("kind" -> kind) ++
   330       JSON.optional("kind" -> kind) ++
   331       JSON.optional("detail" -> detail) ++
   331       JSON.optional("detail" -> detail) ++
   332       JSON.optional("documentation" -> documentation) ++
   332       JSON.optional("documentation" -> documentation) ++
   333       JSON.optional("insertText" -> insertText) ++
   333       JSON.optional("insertText" -> insertText) ++
   334       JSON.optional("range" -> range.map(Range(_)))
   334       JSON.optional("range" -> range.map(Range(_))) ++
       
   335       JSON.optional("textEdit" ->
       
   336         range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label))))
   335   }
   337   }
   336 
   338 
   337   object Completion extends RequestTextDocumentPosition("textDocument/completion")
   339   object Completion extends RequestTextDocumentPosition("textDocument/completion")
   338   {
   340   {
   339     def reply(id: Id, result: List[CompletionItem]): JSON.T =
   341     def reply(id: Id, result: List[CompletionItem]): JSON.T =