Language.LSP.Message.Message

Definitions of messages and associated payloads and responses.

(C) The Idris Community, 2021

Definitions

MessageParams : Method from type -> Type

  Maps the parameters associated to each type of method.

Totality: total
Visibility: public export

ResponseResult : Method from Request -> Type

  Maps the response associated to each type of method.

Totality: total
Visibility: public export

fromMaybeJSONParameters : (method : Method from type) -> Maybe JSON -> Maybe (MessageParams method)

  Parse parameters
  Since the params are sometimes optional we must parse Maybe JSON
  TODO hacky replace with something better

Totality: total
Visibility: export

data NotificationMessage : Method from Notification -> Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#notificationMessage

Totality: total
Visibility: public export
Constructor: 

MkNotificationMessage : (method : Method from Notification) -> MessageParams method -> NotificationMessage method

Hints:

FromJSON (from : MethodFrom ** (method : Method from Notification ** NotificationMessage method))

ToJSON (NotificationMessage method)

method : NotificationMessage m -> Method from Notification

Totality: total
Visibility: export

params : NotificationMessage method -> MessageParams method

Totality: total
Visibility: export

data RequestMessage : Method from Request -> Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#requestMessage

Totality: total
Visibility: public export
Constructor: 

MkRequestMessage : OneOf [Int, String] -> (method : Method from Request) -> MessageParams method -> RequestMessage method

Hints:

FromJSON (from : MethodFrom ** (method : Method from Request ** RequestMessage method))

ToJSON (RequestMessage method)

id : RequestMessage m -> OneOf [Int, String]

Totality: total
Visibility: export

method : RequestMessage m -> Method from Request

Totality: total
Visibility: export

params : RequestMessage method -> MessageParams method

Totality: total
Visibility: export

Message : (type : MethodType) -> Method from type -> Type

  Maps the message payload to each type of method.

Totality: total
Visibility: public export

data ErrorCodes : Type

Totality: total
Visibility: public export
Constructors:

ParseError : ErrorCodes

InvalidRequest : ErrorCodes

MethodNotFound : ErrorCodes

InvalidParams : ErrorCodes

InternalError : ErrorCodes

ServerNotInitialized : ErrorCodes

UnknownErrorCode : ErrorCodes

ContentModified : ErrorCodes

RequestCancelled : ErrorCodes

JSONRPCReserved : Int -> ErrorCodes

LSPReserved : Int -> ErrorCodes

Custom : Int -> ErrorCodes

Hints:

FromJSON ErrorCodes

ToJSON ErrorCodes

record ResponseError : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage

Totality: total
Visibility: public export
Constructor: 

MkResponseError : ErrorCodes -> String -> JSON -> ResponseError

Projections:

.code : ResponseError -> ErrorCodes

.data_ : ResponseError -> JSON

.message : ResponseError -> String

Hints:

FromJSON ResponseError

ToJSON ResponseError

.code : ResponseError -> ErrorCodes

Totality: total
Visibility: public export

code : ResponseError -> ErrorCodes

Totality: total
Visibility: public export

.message : ResponseError -> String

Totality: total
Visibility: public export

message : ResponseError -> String

Totality: total
Visibility: public export

.data_ : ResponseError -> JSON

Totality: total
Visibility: public export

data_ : ResponseError -> JSON

Totality: total
Visibility: public export

data ResponseMessage : Method from type -> Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage

Totality: total
Visibility: public export
Constructors:

Success : OneOf [Int, String, Null] -> ResponseResult method -> ResponseMessage method

Failure : OneOf [Int, String, Null] -> ResponseError -> ResponseMessage method

Hints:

FromJSON (ResponseResult method) => FromJSON (ResponseMessage method)

ToJSON (ResponseMessage method)

id : ResponseMessage method -> OneOf [Int, String, Null]

Totality: total
Visibility: export

getResponseId : RequestMessage method -> OneOf [Int, String, Null]

Totality: total
Visibility: export