# HG changeset patch
# User wenzelm
# Date 1505751081 -7200
# Node ID 6f4613dbfef6c9a492cc465c3e147f56cb645e2e
# Parent  30d5195299e259f9b64066da1f8fa62c49df22b0
support for workspace edits;

diff -r 30d5195299e2 -r 6f4613dbfef6 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Mon Sep 18 10:32:09 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Mon Sep 18 18:11:21 2017 +0200
@@ -62,6 +62,11 @@
 
   /* request message */
 
+  object Id
+  {
+    def empty: Id = Id("")
+  }
+
   sealed case class Id(id: Any)
   {
     require(
@@ -118,6 +123,9 @@
     def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
       if (error == "") apply(id, result = result)
       else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
+
+    def is_empty(json: JSON.T): Boolean =
+      JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined
   }
 
   sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
@@ -324,6 +332,28 @@
   object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
 
 
+  /* workspace edits */
+
+  sealed case class TextEdit(range: Line.Range, new_text: String)
+  {
+    def json: JSON.T = Map("range" -> Range(range), "newText" -> new_text)
+  }
+
+  sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
+  {
+    def json: JSON.T =
+      Map("textDocument" -> Map("uri" -> Url.print_file(file), "version" -> version),
+        "edits" -> edits.map(_.json))
+  }
+
+  object WorkspaceEdit
+  {
+    def apply(edits: List[TextDocumentEdit]): JSON.T =
+      RequestMessage(Id.empty, "workspace/applyEdit",
+        Map("edit" -> Map("documentChanges" -> edits.map(_.json))))
+  }
+
+
   /* completion */
 
   sealed case class CompletionItem(
@@ -342,8 +372,7 @@
       JSON.optional("documentation" -> documentation) ++
       JSON.optional("insertText" -> text) ++
       JSON.optional("range" -> range.map(Range(_))) ++
-      JSON.optional("textEdit" ->
-        range.map(r => Map("range" -> Range(r), "newText" -> text.getOrElse(label)))) ++
+      JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++
       JSON.optional("command" -> command.map(_.json))
   }
 
diff -r 30d5195299e2 -r 6f4613dbfef6 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Sep 18 10:32:09 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:11:21 2017 +0200
@@ -458,7 +458,7 @@
           case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
           case Protocol.Preview_Request(file, column) => request_preview(file, column)
           case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
-          case _ => log("### IGNORED")
+          case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }
       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }