Language.LSP.Message.Command

Definitions

record Command : Type

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

Totality: total
Visibility: public export
Constructor: 

MkCommand : String -> String -> Maybe (List JSON) -> Command

Projections:

.arguments : Command -> Maybe (List JSON)

.command : Command -> String

.title : Command -> String

Hints:

FromJSON Command

ToJSON Command

.title : Command -> String

Totality: total
Visibility: public export

title : Command -> String

Totality: total
Visibility: public export

.command : Command -> String

Totality: total
Visibility: public export

command : Command -> String

Totality: total
Visibility: public export

.arguments : Command -> Maybe (List JSON)

Totality: total
Visibility: public export

arguments : Command -> Maybe (List JSON)

Totality: total
Visibility: public export

record ExecuteCommandClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkExecuteCommandClientCapabilities : Maybe Bool -> ExecuteCommandClientCapabilities

Projection: 

.dynamicRegistration : ExecuteCommandClientCapabilities -> Maybe Bool

Hints:

FromJSON ExecuteCommandClientCapabilities

ToJSON ExecuteCommandClientCapabilities

.dynamicRegistration : ExecuteCommandClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

dynamicRegistration : ExecuteCommandClientCapabilities -> Maybe Bool

Totality: total
Visibility: public export

record ExecuteCommandOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkExecuteCommandOptions : Maybe Bool -> List String -> ExecuteCommandOptions

Projections:

.commands : ExecuteCommandOptions -> List String

.workDoneProgress : ExecuteCommandOptions -> Maybe Bool

Hints:

FromJSON ExecuteCommandOptions

ToJSON ExecuteCommandOptions

.workDoneProgress : ExecuteCommandOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : ExecuteCommandOptions -> Maybe Bool

Totality: total
Visibility: public export

.commands : ExecuteCommandOptions -> List String

Totality: total
Visibility: public export

commands : ExecuteCommandOptions -> List String

Totality: total
Visibility: public export

record ExecuteCommandRegistrationOptions : Type

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

Totality: total
Visibility: public export
Constructor: 

MkExecuteCommandRegistrationOptions : Maybe Bool -> List String -> ExecuteCommandRegistrationOptions

Projections:

.commands : ExecuteCommandRegistrationOptions -> List String

.workDoneProgress : ExecuteCommandRegistrationOptions -> Maybe Bool

Hints:

FromJSON ExecuteCommandRegistrationOptions

ToJSON ExecuteCommandRegistrationOptions

.workDoneProgress : ExecuteCommandRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

workDoneProgress : ExecuteCommandRegistrationOptions -> Maybe Bool

Totality: total
Visibility: public export

.commands : ExecuteCommandRegistrationOptions -> List String

Totality: total
Visibility: public export

commands : ExecuteCommandRegistrationOptions -> List String

Totality: total
Visibility: public export

record ExecuteCommandParams : Type

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

Totality: total
Visibility: public export
Constructor: 

MkExecuteCommandParams : Maybe ProgressToken -> String -> Maybe (List JSON) -> ExecuteCommandParams

Projections:

.arguments : ExecuteCommandParams -> Maybe (List JSON)

.command : ExecuteCommandParams -> String

.partialResultToken : ExecuteCommandParams -> Maybe ProgressToken

Hints:

FromJSON ExecuteCommandParams

ToJSON ExecuteCommandParams

.partialResultToken : ExecuteCommandParams -> Maybe ProgressToken

Totality: total
Visibility: public export

partialResultToken : ExecuteCommandParams -> Maybe ProgressToken

Totality: total
Visibility: public export

.command : ExecuteCommandParams -> String

Totality: total
Visibility: public export

command : ExecuteCommandParams -> String

Totality: total
Visibility: public export

.arguments : ExecuteCommandParams -> Maybe (List JSON)

Totality: total
Visibility: public export

arguments : ExecuteCommandParams -> Maybe (List JSON)

Totality: total
Visibility: public export