support for workspace edits;
authorwenzelm
Mon Sep 18 18:11:21 2017 +0200 (21 months ago)
changeset 666756f4613dbfef6
parent 66674 30d5195299e2
child 66676 39db5bb7eb0a
support for workspace edits;
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/src/protocol.scala	Mon Sep 18 10:32:09 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/protocol.scala	Mon Sep 18 18:11:21 2017 +0200
     1.3 @@ -62,6 +62,11 @@
     1.4  
     1.5    /* request message */
     1.6  
     1.7 +  object Id
     1.8 +  {
     1.9 +    def empty: Id = Id("")
    1.10 +  }
    1.11 +
    1.12    sealed case class Id(id: Any)
    1.13    {
    1.14      require(
    1.15 @@ -118,6 +123,9 @@
    1.16      def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
    1.17        if (error == "") apply(id, result = result)
    1.18        else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
    1.19 +
    1.20 +    def is_empty(json: JSON.T): Boolean =
    1.21 +      JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined
    1.22    }
    1.23  
    1.24    sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
    1.25 @@ -324,6 +332,28 @@
    1.26    object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
    1.27  
    1.28  
    1.29 +  /* workspace edits */
    1.30 +
    1.31 +  sealed case class TextEdit(range: Line.Range, new_text: String)
    1.32 +  {
    1.33 +    def json: JSON.T = Map("range" -> Range(range), "newText" -> new_text)
    1.34 +  }
    1.35 +
    1.36 +  sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
    1.37 +  {
    1.38 +    def json: JSON.T =
    1.39 +      Map("textDocument" -> Map("uri" -> Url.print_file(file), "version" -> version),
    1.40 +        "edits" -> edits.map(_.json))
    1.41 +  }
    1.42 +
    1.43 +  object WorkspaceEdit
    1.44 +  {
    1.45 +    def apply(edits: List[TextDocumentEdit]): JSON.T =
    1.46 +      RequestMessage(Id.empty, "workspace/applyEdit",
    1.47 +        Map("edit" -> Map("documentChanges" -> edits.map(_.json))))
    1.48 +  }
    1.49 +
    1.50 +
    1.51    /* completion */
    1.52  
    1.53    sealed case class CompletionItem(
    1.54 @@ -342,8 +372,7 @@
    1.55        JSON.optional("documentation" -> documentation) ++
    1.56        JSON.optional("insertText" -> text) ++
    1.57        JSON.optional("range" -> range.map(Range(_))) ++
    1.58 -      JSON.optional("textEdit" ->
    1.59 -        range.map(r => Map("range" -> Range(r), "newText" -> text.getOrElse(label)))) ++
    1.60 +      JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++
    1.61        JSON.optional("command" -> command.map(_.json))
    1.62    }
    1.63  
     2.1 --- a/src/Tools/VSCode/src/server.scala	Mon Sep 18 10:32:09 2017 +0200
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:11:21 2017 +0200
     2.3 @@ -458,7 +458,7 @@
     2.4            case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
     2.5            case Protocol.Preview_Request(file, column) => request_preview(file, column)
     2.6            case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
     2.7 -          case _ => log("### IGNORED")
     2.8 +          case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED")
     2.9          }
    2.10        }
    2.11        catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }