src/Tools/VSCode/src/protocol.scala
changeset 66675 6f4613dbfef6
parent 66235 d4fa51e7c4ff
child 67813 3e226d3b7bc6
     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