src/Tools/VSCode/src/protocol.scala
author wenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622 529bbb8977c7
parent 64605 9c1173a7e4cb
child 64648 5d7f741aaccb
permissions -rw-r--r--
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm@64605
     1
/*  Title:      Tools/VSCode/src/protocol.scala
wenzelm@64605
     2
    Author:     Makarius
wenzelm@64605
     3
wenzelm@64605
     4
Message formats for Language Server Protocol 2.0, see
wenzelm@64605
     5
https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
wenzelm@64605
     6
*/
wenzelm@64605
     7
wenzelm@64605
     8
package isabelle.vscode
wenzelm@64605
     9
wenzelm@64605
    10
wenzelm@64605
    11
import isabelle._
wenzelm@64605
    12
wenzelm@64605
    13
wenzelm@64605
    14
object Protocol
wenzelm@64605
    15
{
wenzelm@64605
    16
  /* abstract message */
wenzelm@64605
    17
wenzelm@64605
    18
  object Message
wenzelm@64605
    19
  {
wenzelm@64605
    20
    val empty: Map[String, JSON.T] = Map("jsonrpc" -> "2.0")
wenzelm@64605
    21
  }
wenzelm@64605
    22
wenzelm@64605
    23
wenzelm@64605
    24
  /* notification */
wenzelm@64605
    25
wenzelm@64605
    26
  object Notification
wenzelm@64605
    27
  {
wenzelm@64605
    28
    def apply(method: String, params: JSON.T): JSON.T =
wenzelm@64605
    29
      Message.empty + ("method" -> method) + ("params" -> params)
wenzelm@64605
    30
wenzelm@64605
    31
    def unapply(json: JSON.T): Option[(String, Option[JSON.T])] =
wenzelm@64605
    32
      for {
wenzelm@64605
    33
        method <- JSON.string(json, "method")
wenzelm@64605
    34
        params = JSON.value(json, "params")
wenzelm@64605
    35
      } yield (method, params)
wenzelm@64605
    36
  }
wenzelm@64605
    37
wenzelm@64605
    38
  class Notification0(name: String)
wenzelm@64605
    39
  {
wenzelm@64605
    40
    def unapply(json: JSON.T): Option[Unit] =
wenzelm@64605
    41
      json match {
wenzelm@64605
    42
        case Notification(method, _) if method == name => Some(())
wenzelm@64605
    43
        case _ => None
wenzelm@64605
    44
      }
wenzelm@64605
    45
  }
wenzelm@64605
    46
wenzelm@64605
    47
wenzelm@64605
    48
  /* request message */
wenzelm@64605
    49
wenzelm@64605
    50
  sealed case class Id(id: Any)
wenzelm@64605
    51
  {
wenzelm@64605
    52
    require(
wenzelm@64605
    53
      id.isInstanceOf[Int] ||
wenzelm@64605
    54
      id.isInstanceOf[Long] ||
wenzelm@64605
    55
      id.isInstanceOf[Double] ||
wenzelm@64605
    56
      id.isInstanceOf[String])
wenzelm@64605
    57
wenzelm@64605
    58
    override def toString: String = id.toString
wenzelm@64605
    59
  }
wenzelm@64605
    60
wenzelm@64605
    61
  object RequestMessage
wenzelm@64605
    62
  {
wenzelm@64605
    63
    def apply(id: Id, method: String, params: JSON.T): JSON.T =
wenzelm@64605
    64
      Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params)
wenzelm@64605
    65
wenzelm@64605
    66
    def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] =
wenzelm@64605
    67
      for {
wenzelm@64605
    68
        id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id")
wenzelm@64605
    69
        method <- JSON.string(json, "method")
wenzelm@64605
    70
        params = JSON.value(json, "params")
wenzelm@64605
    71
      } yield (Id(id), method, params)
wenzelm@64605
    72
  }
wenzelm@64605
    73
wenzelm@64605
    74
  class Request0(name: String)
wenzelm@64605
    75
  {
wenzelm@64605
    76
    def unapply(json: JSON.T): Option[Id] =
wenzelm@64605
    77
      json match {
wenzelm@64605
    78
        case RequestMessage(id, method, _) if method == name => Some(id)
wenzelm@64605
    79
        case _ => None
wenzelm@64605
    80
      }
wenzelm@64605
    81
  }
wenzelm@64605
    82
wenzelm@64605
    83
wenzelm@64605
    84
  /* response message */
wenzelm@64605
    85
wenzelm@64605
    86
  object ResponseMessage
wenzelm@64605
    87
  {
wenzelm@64605
    88
    def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
wenzelm@64605
    89
      Message.empty + ("id" -> id.id) ++
wenzelm@64605
    90
      (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++
wenzelm@64605
    91
      (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty })
wenzelm@64605
    92
wenzelm@64605
    93
    def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
wenzelm@64605
    94
      if (error == "") apply(id, result = result)
wenzelm@64605
    95
      else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
wenzelm@64605
    96
  }
wenzelm@64605
    97
wenzelm@64605
    98
  sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
wenzelm@64605
    99
  {
wenzelm@64605
   100
    def json: JSON.T =
wenzelm@64605
   101
      Map("code" -> code, "message" -> message) ++
wenzelm@64605
   102
      (data match { case Some(x) => Map("data" -> x) case None => Map.empty })
wenzelm@64605
   103
  }
wenzelm@64605
   104
wenzelm@64605
   105
  object ErrorCodes
wenzelm@64605
   106
  {
wenzelm@64605
   107
    val ParseError = -32700
wenzelm@64605
   108
    val InvalidRequest = -32600
wenzelm@64605
   109
    val MethodNotFound = -32601
wenzelm@64605
   110
    val InvalidParams = -32602
wenzelm@64605
   111
    val InternalError = -32603
wenzelm@64605
   112
    val serverErrorStart = -32099
wenzelm@64605
   113
    val serverErrorEnd = -32000
wenzelm@64605
   114
  }
wenzelm@64605
   115
wenzelm@64605
   116
wenzelm@64605
   117
  /* init and exit */
wenzelm@64605
   118
wenzelm@64605
   119
  object Initialize extends Request0("initialize")
wenzelm@64605
   120
  {
wenzelm@64605
   121
    def reply(id: Id, error: String): JSON.T =
wenzelm@64605
   122
      ResponseMessage.strict(id, Some(Map("capabilities" -> ServerCapabilities.json)), error)
wenzelm@64605
   123
  }
wenzelm@64605
   124
wenzelm@64605
   125
  object ServerCapabilities
wenzelm@64605
   126
  {
wenzelm@64605
   127
    val json: JSON.T =
wenzelm@64605
   128
      Map("textDocumentSync" -> 1, "hoverProvider" -> true)
wenzelm@64605
   129
  }
wenzelm@64605
   130
wenzelm@64605
   131
  object Shutdown extends Request0("shutdown")
wenzelm@64605
   132
  {
wenzelm@64605
   133
    def reply(id: Id, error: String): JSON.T =
wenzelm@64605
   134
      ResponseMessage.strict(id, Some("OK"), error)
wenzelm@64605
   135
  }
wenzelm@64605
   136
wenzelm@64605
   137
  object Exit extends Notification0("exit")
wenzelm@64605
   138
wenzelm@64605
   139
wenzelm@64605
   140
  /* document positions */
wenzelm@64605
   141
wenzelm@64605
   142
  object Position
wenzelm@64605
   143
  {
wenzelm@64605
   144
    def apply(pos: Line.Position): JSON.T =
wenzelm@64605
   145
      Map("line" -> pos.line, "character" -> pos.column)
wenzelm@64605
   146
wenzelm@64605
   147
    def unapply(json: JSON.T): Option[Line.Position] =
wenzelm@64605
   148
      for {
wenzelm@64605
   149
        line <- JSON.int(json, "line")
wenzelm@64605
   150
        column <- JSON.int(json, "character")
wenzelm@64605
   151
      } yield Line.Position(line, column)
wenzelm@64605
   152
  }
wenzelm@64605
   153
wenzelm@64605
   154
  object Range
wenzelm@64605
   155
  {
wenzelm@64605
   156
    def apply(range: Line.Range): JSON.T =
wenzelm@64605
   157
      Map("start" -> Position(range.start), "end" -> Position(range.stop))
wenzelm@64605
   158
wenzelm@64605
   159
    def unapply(json: JSON.T): Option[Line.Range] =
wenzelm@64605
   160
      (JSON.value(json, "start"), JSON.value(json, "end")) match {
wenzelm@64605
   161
        case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop))
wenzelm@64605
   162
        case _ => None
wenzelm@64605
   163
      }
wenzelm@64605
   164
  }
wenzelm@64605
   165
wenzelm@64605
   166
  object Location
wenzelm@64605
   167
  {
wenzelm@64605
   168
    def apply(uri: String, range: Line.Range): JSON.T =
wenzelm@64605
   169
      Map("uri" -> uri, "range" -> Range(range))
wenzelm@64605
   170
wenzelm@64605
   171
    def unapply(json: JSON.T): Option[(String, Line.Range)] =
wenzelm@64605
   172
      for {
wenzelm@64605
   173
        uri <- JSON.string(json, "uri")
wenzelm@64605
   174
        range_json <- JSON.value(json, "range")
wenzelm@64605
   175
        range <- Range.unapply(range_json)
wenzelm@64605
   176
      } yield (uri, range)
wenzelm@64605
   177
  }
wenzelm@64605
   178
wenzelm@64605
   179
  object TextDocumentPosition
wenzelm@64605
   180
  {
wenzelm@64605
   181
    def unapply(json: JSON.T): Option[(String, Line.Position)] =
wenzelm@64605
   182
      for {
wenzelm@64605
   183
        doc <- JSON.value(json, "textDocument")
wenzelm@64605
   184
        uri <- JSON.string(doc, "uri")
wenzelm@64605
   185
        pos_json <- JSON.value(json, "position")
wenzelm@64605
   186
        pos <- Position.unapply(pos_json)
wenzelm@64605
   187
      } yield (uri, pos)
wenzelm@64605
   188
  }
wenzelm@64605
   189
wenzelm@64605
   190
wenzelm@64605
   191
  /* diagnostic messages */
wenzelm@64605
   192
wenzelm@64605
   193
  object MessageType
wenzelm@64605
   194
  {
wenzelm@64605
   195
    val Error = 1
wenzelm@64605
   196
    val Warning = 2
wenzelm@64605
   197
    val Info = 3
wenzelm@64605
   198
    val Log = 4
wenzelm@64605
   199
  }
wenzelm@64605
   200
wenzelm@64605
   201
  object DisplayMessage
wenzelm@64605
   202
  {
wenzelm@64605
   203
    def apply(message_type: Int, message: String, show: Boolean = true): JSON.T =
wenzelm@64605
   204
      Notification(if (show) "window/showMessage" else "window/logMessage",
wenzelm@64605
   205
        Map("type" -> message_type, "message" -> message))
wenzelm@64605
   206
  }
wenzelm@64605
   207
wenzelm@64605
   208
wenzelm@64605
   209
  /* document edits */
wenzelm@64605
   210
wenzelm@64605
   211
  object DidOpenTextDocument
wenzelm@64605
   212
  {
wenzelm@64605
   213
    def unapply(json: JSON.T): Option[(String, String, Long, String)] =
wenzelm@64605
   214
      json match {
wenzelm@64605
   215
        case Notification("textDocument/didOpen", Some(params)) =>
wenzelm@64605
   216
          for {
wenzelm@64605
   217
            doc <- JSON.value(params, "textDocument")
wenzelm@64605
   218
            uri <- JSON.string(doc, "uri")
wenzelm@64605
   219
            lang <- JSON.string(doc, "languageId")
wenzelm@64605
   220
            version <- JSON.long(doc, "version")
wenzelm@64605
   221
            text <- JSON.string(doc, "text")
wenzelm@64605
   222
          } yield (uri, lang, version, text)
wenzelm@64605
   223
        case _ => None
wenzelm@64605
   224
      }
wenzelm@64605
   225
  }
wenzelm@64605
   226
wenzelm@64605
   227
wenzelm@64605
   228
  sealed abstract class TextDocumentContentChange
wenzelm@64605
   229
  case class TextDocumentContent(text: String) extends TextDocumentContentChange
wenzelm@64605
   230
  case class TextDocumentChange(range: Line.Range, range_length: Int, text: String)
wenzelm@64605
   231
    extends TextDocumentContentChange
wenzelm@64605
   232
wenzelm@64605
   233
  object TextDocumentContentChange
wenzelm@64605
   234
  {
wenzelm@64605
   235
    def unapply(json: JSON.T): Option[TextDocumentContentChange] =
wenzelm@64605
   236
      for { text <- JSON.string(json, "text") }
wenzelm@64605
   237
      yield {
wenzelm@64605
   238
        (JSON.value(json, "range"), JSON.int(json, "rangeLength")) match {
wenzelm@64605
   239
          case (Some(Range(range)), Some(range_length)) =>
wenzelm@64605
   240
            TextDocumentChange(range, range_length, text)
wenzelm@64605
   241
          case _ => TextDocumentContent(text)
wenzelm@64605
   242
        }
wenzelm@64605
   243
      }
wenzelm@64605
   244
  }
wenzelm@64605
   245
wenzelm@64605
   246
  object DidChangeTextDocument
wenzelm@64605
   247
  {
wenzelm@64605
   248
    def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] =
wenzelm@64605
   249
      json match {
wenzelm@64605
   250
        case Notification("textDocument/didChange", Some(params)) =>
wenzelm@64605
   251
          for {
wenzelm@64605
   252
            doc <- JSON.value(params, "textDocument")
wenzelm@64605
   253
            uri <- JSON.string(doc, "uri")
wenzelm@64605
   254
            version <- JSON.long(doc, "version")
wenzelm@64605
   255
            changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
wenzelm@64605
   256
          } yield (uri, version, changes)
wenzelm@64605
   257
        case _ => None
wenzelm@64605
   258
      }
wenzelm@64605
   259
  }
wenzelm@64605
   260
wenzelm@64605
   261
  class TextDocumentNotification(name: String)
wenzelm@64605
   262
  {
wenzelm@64605
   263
    def unapply(json: JSON.T): Option[String] =
wenzelm@64605
   264
      json match {
wenzelm@64605
   265
        case Notification(method, Some(params)) if method == name =>
wenzelm@64605
   266
          for {
wenzelm@64605
   267
            doc <- JSON.value(params, "textDocument")
wenzelm@64605
   268
            uri <- JSON.string(doc, "uri")
wenzelm@64605
   269
          } yield uri
wenzelm@64605
   270
        case _ => None
wenzelm@64605
   271
      }
wenzelm@64605
   272
  }
wenzelm@64605
   273
wenzelm@64605
   274
  object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose")
wenzelm@64605
   275
  object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
wenzelm@64605
   276
wenzelm@64605
   277
wenzelm@64605
   278
  /* hover request */
wenzelm@64605
   279
wenzelm@64605
   280
  object Hover
wenzelm@64605
   281
  {
wenzelm@64605
   282
    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
wenzelm@64605
   283
      json match {
wenzelm@64605
   284
        case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) =>
wenzelm@64605
   285
          Some((id, uri, pos))
wenzelm@64605
   286
        case _ => None
wenzelm@64605
   287
      }
wenzelm@64605
   288
wenzelm@64605
   289
    def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
wenzelm@64605
   290
    {
wenzelm@64605
   291
      val res =
wenzelm@64605
   292
        result match {
wenzelm@64605
   293
          case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
wenzelm@64605
   294
          case None => Map("contents" -> Nil)
wenzelm@64605
   295
        }
wenzelm@64605
   296
      ResponseMessage(id, Some(res))
wenzelm@64605
   297
    }
wenzelm@64605
   298
  }
wenzelm@64605
   299
}