0 | module Language.LSP.Message.Rename
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Location
 5 | import Language.LSP.Message.Progress
 6 | import Language.LSP.Message.TextDocument
 7 | import Language.LSP.Message.Utils
 8 | import Language.Reflection
 9 |
10 | %language ElabReflection
11 | %default total
12 |
13 | namespace PrepareSupportDefaultBehaviour
14 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
15 |   public export
16 |   data PrepareSupportDefaultBehaviour = Identifier
17 |
18 | export
19 | ToJSON PrepareSupportDefaultBehaviour where
20 |   toJSON Identifier = JNumber 1
21 |
22 | export
23 | FromJSON PrepareSupportDefaultBehaviour where
24 |   fromJSON (JNumber 1) = pure Identifier
25 |   fromJSON _ = neutral
26 |
27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
28 | public export
29 | record RenameClientCapabilities where
30 |   constructor MkRenameClientCapabilities
31 |   dynamicRegistration            : Maybe Bool
32 |   prepareSupport                 : Maybe Bool
33 |   prepareSupportDefaultBehaviour : Maybe PrepareSupportDefaultBehaviour
34 |   honorsChangeAnnotation         : Maybe Bool
35 | %runElab deriveJSON defaultOpts `{RenameClientCapabilities}
36 |
37 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
38 | public export
39 | record RenameOptions where
40 |   constructor MkRenameOptions
41 |   workDoneProgress : Maybe Bool
42 |   prepareProvider  : Maybe Bool
43 | %runElab deriveJSON defaultOpts `{RenameOptions}
44 |
45 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
46 | public export
47 | record RenameRegistrationOptions where
48 |   constructor MkRenameRegistrationOptions
49 |   workDoneProgress : Maybe Bool
50 |   prepareProvider  : Maybe Bool
51 |   documentSelector : OneOf [DocumentSelector, Null]
52 | %runElab deriveJSON defaultOpts `{RenameRegistrationOptions}
53 |
54 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
55 | public export
56 | record RenameParams where
57 |   constructor MkRenameParams
58 |   workDoneToken : Maybe ProgressToken
59 |   textDocument  : TextDocumentIdentifier
60 |   newName       : String
61 | %runElab deriveJSON defaultOpts `{RenameParams}
62 |
63 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename
64 | public export
65 | record PrepareRenameParams where
66 |   constructor MkPrepareRenameParams
67 |   textDocument : TextDocumentIdentifier
68 |   position     : Position
69 | %runElab deriveJSON defaultOpts `{PrepareRenameParams}
70 |
71 | namespace PrepareRenameResponse
72 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename
73 |   public export
74 |   record PrepareRenameDefaultResponse where
75 |     constructor MkPrepareRenameDefaultResponse
76 |     defaultBehaviour : Bool
77 |   %runElab deriveJSON defaultOpts `{PrepareRenameDefaultResponse}
78 |
79 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename
80 |   public export
81 |   record PrepareRenamePlaceholderResponse where
82 |     constructor MkPrepareRenamePlaceholderResponse
83 |     range       : Range
84 |     placeholder : String
85 |   %runElab deriveJSON defaultOpts `{PrepareRenamePlaceholderResponse}
86 |