0 | module Language.LSP.Message.CodeAction
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.Command
  4 | import Language.LSP.Message.Derive
  5 | import Language.LSP.Message.Diagnostics
  6 | import Language.LSP.Message.Location
  7 | import Language.LSP.Message.Progress
  8 | import Language.LSP.Message.TextDocument
  9 | import Language.LSP.Message.URI
 10 | import Language.LSP.Message.Utils
 11 | import Language.LSP.Message.Workspace
 12 | import Language.Reflection
 13 |
 14 | %language ElabReflection
 15 | %default total
 16 |
 17 | namespace CodeActionKind
 18 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
 19 |   public export
 20 |   data CodeActionKind
 21 |     = Empty
 22 |     | QuickFix
 23 |     | Refactor
 24 |     | RefactorExtract
 25 |     | RefactorInline
 26 |     | RefactorRewrite
 27 |     | Source
 28 |     | SourceOrganizeImport
 29 |     | Other String
 30 |
 31 | export
 32 | Eq CodeActionKind where
 33 |   Empty == Empty = True
 34 |   QuickFix == QuickFix = True
 35 |   Refactor == Refactor = True
 36 |   RefactorExtract == RefactorExtract = True
 37 |   RefactorInline == RefactorInline = True
 38 |   RefactorRewrite == RefactorRewrite = True
 39 |   Source == Source = True
 40 |   SourceOrganizeImport == SourceOrganizeImport = True
 41 |   (Other str) == (Other str') = str == str'
 42 |   _ == _ = False
 43 |
 44 | export
 45 | ToJSON CodeActionKind where
 46 |   toJSON Empty                = JString ""
 47 |   toJSON QuickFix             = JString "quickfix"
 48 |   toJSON Refactor             = JString "refactor"
 49 |   toJSON RefactorExtract      = JString "refactor.extract"
 50 |   toJSON RefactorInline       = JString "refactor.inline"
 51 |   toJSON RefactorRewrite      = JString "refactor.rewrite"
 52 |   toJSON Source               = JString "source"
 53 |   toJSON SourceOrganizeImport = JString "source.organizeImports"
 54 |   toJSON (Other act)          = JString act
 55 |
 56 | export
 57 | FromJSON CodeActionKind where
 58 |   fromJSON (JString "")                       = pure Empty
 59 |   fromJSON (JString "quickfix")               = pure QuickFix
 60 |   fromJSON (JString "refactor")               = pure Refactor
 61 |   fromJSON (JString "refactor.extract")       = pure RefactorExtract
 62 |   fromJSON (JString "refactor.inline")        = pure RefactorInline
 63 |   fromJSON (JString "refactor.rewrite")       = pure RefactorRewrite
 64 |   fromJSON (JString "source")                 = pure Source
 65 |   fromJSON (JString "source.organizeImports") = pure SourceOrganizeImport
 66 |   fromJSON (JString act)                      = pure (Other act)
 67 |   fromJSON _ = neutral
 68 |
 69 | namespace CodeActionClientCapabilities
 70 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
 71 |   public export
 72 |   record CodeActionKindValueSet where
 73 |     constructor MkCodeActionKindValueSet
 74 |     valueSet : List CodeActionKind
 75 |   %runElab deriveJSON defaultOpts `{CodeActionKindValueSet}
 76 |
 77 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
 78 |   public export
 79 |   record CodeActionLiteralSupport where
 80 |     constructor MkCodeActionLiteralSupport
 81 |     codeActionKind : CodeActionKindValueSet
 82 |   %runElab deriveJSON defaultOpts `{CodeActionLiteralSupport}
 83 |
 84 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
 85 |   public export
 86 |   record ResolveSupport where
 87 |     constructor MkResolveSupport
 88 |     properties : List String
 89 |   %runElab deriveJSON defaultOpts `{ResolveSupport}
 90 |
 91 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
 92 | public export
 93 | record CodeActionClientCapabilities where
 94 |   constructor MkCodeActionClientCapabilities
 95 |   dynamicRegistration      : Maybe Bool
 96 |   codeActionLiteralSupport : Maybe CodeActionLiteralSupport
 97 |   isPreferredSupport       : Maybe Bool
 98 |   disabledSupport          : Maybe Bool
 99 |   dataSupport              : Maybe Bool
100 |   resolveSupport           : Maybe ResolveSupport
101 |   honorsChangeAnnotations  : Maybe Bool
102 | %runElab deriveJSON defaultOpts `{CodeActionClientCapabilities}
103 |
104 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
105 | public export
106 | record CodeActionOptions where
107 |   constructor MkCodeActionOptions
108 |   workDoneProgress : Maybe Bool
109 |   codeActionKinds  : Maybe (List CodeActionKind)
110 |   resolveProvider  : Maybe Bool
111 | %runElab deriveJSON defaultOpts `{CodeActionOptions}
112 |
113 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
114 | public export
115 | record CodeActionRegistrationOptions where
116 |   constructor MkCodeActionRegistrationOptions
117 |   workDoneProgress : Maybe Bool
118 |   codeActionKinds  : Maybe (List CodeActionKind)
119 |   resolveProvider  : Maybe Bool
120 |   documentSelector : OneOf [DocumentSelector, Null]
121 | %runElab deriveJSON defaultOpts `{CodeActionRegistrationOptions}
122 |
123 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
124 | public export
125 | record CodeActionContext where
126 |   constructor MkCodeActionContext
127 |   diagnostics : List Diagnostic
128 |   only        : Maybe (List CodeActionKind)
129 | %runElab deriveJSON defaultOpts `{CodeActionContext}
130 |
131 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
132 | public export
133 | record CodeActionParams where
134 |   constructor MkCodeActionParams
135 |   workDoneToken      : Maybe ProgressToken
136 |   partialResultToken : Maybe ProgressToken
137 |   textDocument       : TextDocumentIdentifier
138 |   range              : Range
139 |   context            : CodeActionContext
140 | %runElab deriveJSON defaultOpts `{CodeActionParams}
141 |
142 | namespace CodeAction
143 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
144 |   public export
145 |   record Disabled where
146 |     constructor MkDisabled
147 |     reason : String
148 |   %runElab deriveJSON defaultOpts `{Disabled}
149 |
150 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
151 | public export
152 | record CodeAction where
153 |   constructor MkCodeAction
154 |   title       : String
155 |   kind        : Maybe CodeActionKind
156 |   diagnostics : Maybe (List Diagnostic)
157 |   isPreferred : Maybe Bool
158 |   disabled    : Maybe Disabled
159 |   edit        : Maybe WorkspaceEdit
160 |   command     : Maybe Command
161 |   data_       : Maybe JSON
162 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CodeAction}
163 |