Language.LSP.Message.Registration

Definitions

record Registration : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRegistration : String -> String -> Maybe JSON -> Registration

Projections:

.id : Registration -> String

.method : Registration -> String

.registerOptions : Registration -> Maybe JSON

Hints:

FromJSON Registration

ToJSON Registration

.id : Registration -> String

Totality: total
Visibility: public export

id : Registration -> String

Totality: total
Visibility: public export

.method : Registration -> String

Totality: total
Visibility: public export

method : Registration -> String

Totality: total
Visibility: public export

.registerOptions : Registration -> Maybe JSON

Totality: total
Visibility: public export

registerOptions : Registration -> Maybe JSON

Totality: total
Visibility: public export

record RegistrationParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRegistrationParams : List Registration -> RegistrationParams

Projection: 

.registrations : RegistrationParams -> List Registration

Hints:

FromJSON RegistrationParams

ToJSON RegistrationParams

.registrations : RegistrationParams -> List Registration

Totality: total
Visibility: public export

registrations : RegistrationParams -> List Registration

Totality: total
Visibility: public export

record Unregistration : Type

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

Totality: total
Visibility: public export
Constructor: 

MkUnregistration : String -> String -> Unregistration

Projections:

.id : Unregistration -> String

.method : Unregistration -> String

Hints:

FromJSON Unregistration

ToJSON Unregistration

.id : Unregistration -> String

Totality: total
Visibility: public export

id : Unregistration -> String

Totality: total
Visibility: public export

.method : Unregistration -> String

Totality: total
Visibility: public export

method : Unregistration -> String

Totality: total
Visibility: public export

record UnregistrationParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkUnregistrationParams : List Unregistration -> UnregistrationParams

Projection: 

.unregisterations : UnregistrationParams -> List Unregistration

Hints:

FromJSON UnregistrationParams

ToJSON UnregistrationParams

.unregisterations : UnregistrationParams -> List Unregistration

Totality: total
Visibility: public export

unregisterations : UnregistrationParams -> List Unregistration

Totality: total
Visibility: public export