0 | module Language.LSP.Message.Command
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Progress
 5 | import Language.LSP.Message.Utils
 6 | import Language.Reflection
 7 |
 8 | %language ElabReflection
 9 | %default total
10 |
11 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#command
12 | public export
13 | record Command where
14 |   constructor MkCommand
15 |   title     : String
16 |   command   : String
17 |   arguments : Maybe (List JSON)
18 | %runElab deriveJSON defaultOpts `{Command}
19 |
20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
21 | public export
22 | record ExecuteCommandClientCapabilities where
23 |   constructor MkExecuteCommandClientCapabilities
24 |   dynamicRegistration : Maybe Bool
25 | %runElab deriveJSON defaultOpts `{ExecuteCommandClientCapabilities}
26 |
27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
28 | public export
29 | record ExecuteCommandOptions where
30 |   constructor MkExecuteCommandOptions
31 |   workDoneProgress : Maybe Bool
32 |   commands         : List String
33 | %runElab deriveJSON defaultOpts `{ExecuteCommandOptions}
34 |
35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
36 | public export
37 | record ExecuteCommandRegistrationOptions where
38 |   constructor MkExecuteCommandRegistrationOptions
39 |   workDoneProgress : Maybe Bool
40 |   commands         : List String
41 | %runElab deriveJSON defaultOpts `{ExecuteCommandRegistrationOptions}
42 |
43 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
44 | public export
45 | record ExecuteCommandParams where
46 |   constructor MkExecuteCommandParams
47 |   partialResultToken : Maybe ProgressToken
48 |   command            : String
49 |   arguments          : Maybe (List JSON)
50 | %runElab deriveJSON defaultOpts `{ExecuteCommandParams}
51 |