src/Tools/VSCode/src/protocol.scala
changeset 64878 e9208a9301c0
parent 64877 31e9920a0dc1
child 65093 5f08197206ce
equal deleted inserted replaced
64877:31e9920a0dc1 64878:e9208a9301c0
    98 
    98 
    99   object ResponseMessage
    99   object ResponseMessage
   100   {
   100   {
   101     def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
   101     def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
   102       Message.empty + ("id" -> id.id) ++
   102       Message.empty + ("id" -> id.id) ++
   103       (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++
   103         JSON.optional("result" -> result) ++
   104       (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty })
   104         JSON.optional("error" -> error.map(_.json))
   105 
   105 
   106     def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
   106     def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
   107       if (error == "") apply(id, result = result)
   107       if (error == "") apply(id, result = result)
   108       else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
   108       else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
   109   }
   109   }
   110 
   110 
   111   sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
   111   sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
   112   {
   112   {
   113     def json: JSON.T =
   113     def json: JSON.T =
   114       Map("code" -> code, "message" -> message) ++
   114       Map("code" -> code, "message" -> message) ++ JSON.optional("data" -> data)
   115       (data match { case Some(x) => Map("data" -> x) case None => Map.empty })
       
   116   }
   115   }
   117 
   116 
   118   object ErrorCodes
   117   object ErrorCodes
   119   {
   118   {
   120     val ParseError = -32700
   119     val ParseError = -32700
   303     insertText: Option[String] = None,
   302     insertText: Option[String] = None,
   304     range: Option[Line.Range] = None)
   303     range: Option[Line.Range] = None)
   305   {
   304   {
   306     def json: JSON.T =
   305     def json: JSON.T =
   307       Message.empty + ("label" -> label) ++
   306       Message.empty + ("label" -> label) ++
   308       (kind match { case Some(x) => Map("kind" -> x) case None => Map.empty }) ++
   307         JSON.optional("kind" -> kind) ++
   309       (detail match { case Some(x) => Map("detail" -> x) case None => Map.empty }) ++
   308         JSON.optional("detail" -> detail) ++
   310       (documentation match { case Some(x) => Map("documentation" -> x) case None => Map.empty }) ++
   309         JSON.optional("documentation" -> documentation) ++
   311       (insertText match { case Some(x) => Map("insertText" -> x) case None => Map.empty }) ++
   310         JSON.optional("insertText" -> insertText) ++
   312       (range match { case Some(x) => Map("range" -> Range(x)) case None => Map.empty })
   311         JSON.optional("range" -> range.map(Range(_)))
   313   }
   312   }
   314 
   313 
   315   object Completion extends RequestTextDocumentPosition("textDocument/completion")
   314   object Completion extends RequestTextDocumentPosition("textDocument/completion")
   316   {
   315   {
   317     def reply(id: Id, result: List[CompletionItem]): JSON.T =
   316     def reply(id: Id, result: List[CompletionItem]): JSON.T =
   376   sealed case class Diagnostic(range: Line.Range, message: String,
   375   sealed case class Diagnostic(range: Line.Range, message: String,
   377     severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
   376     severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
   378   {
   377   {
   379     def json: JSON.T =
   378     def json: JSON.T =
   380       Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
   379       Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
   381       (severity match { case Some(x) => Map("severity" -> x) case None => Map.empty }) ++
   380       JSON.optional("severity" -> severity) ++
   382       (code match { case Some(x) => Map("code" -> x) case None => Map.empty }) ++
   381       JSON.optional("code" -> code) ++
   383       (source match { case Some(x) => Map("source" -> x) case None => Map.empty })
   382       JSON.optional("source" -> source)
   384   }
   383   }
   385 
   384 
   386   object DiagnosticSeverity
   385   object DiagnosticSeverity
   387   {
   386   {
   388     val Error = 1
   387     val Error = 1