0 | module Language.LSP.Message.Registration
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Utils
 5 | import Language.Reflection
 6 |
 7 | %language ElabReflection
 8 | %default total
 9 |
10 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_registerCapability
11 | public export
12 | record Registration where
13 |   constructor MkRegistration
14 |   id              : String
15 |   method          : String
16 |   registerOptions : Maybe JSON
17 | %runElab deriveJSON defaultOpts `{Registration}
18 |
19 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_registerCapability
20 | public export
21 | record RegistrationParams where
22 |   constructor MkRegistrationParams
23 |   registrations : List Registration
24 | %runElab deriveJSON defaultOpts `{RegistrationParams}
25 |
26 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_unregisterCapability
27 | public export
28 | record Unregistration where
29 |   constructor MkUnregistration
30 |   id     : String
31 |   method : String
32 | %runElab deriveJSON defaultOpts `{Unregistration}
33 |
34 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_unregisterCapability
35 | public export
36 | record UnregistrationParams where
37 |   constructor MkUnregistrationParams
38 |   -- NOTE: not my typo, but see the specification link in the record documentation
39 |   unregisterations : List Unregistration
40 | %runElab deriveJSON defaultOpts `{UnregistrationParams}
41 |