0 | module Language.LSP.Message.Hover
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Location
 5 | import Language.LSP.Message.Markup
 6 | import Language.LSP.Message.Progress
 7 | import Language.LSP.Message.TextDocument
 8 | import Language.LSP.Message.Utils
 9 | import Language.Reflection
10 |
11 | %language ElabReflection
12 | %default total
13 |
14 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
15 | public export
16 | record HoverClientCapabilities where
17 |   constructor MkHoverClientCapabilities
18 |   dynamicRegistration : Maybe Bool
19 |   contentFormat : Maybe (List MarkupKind)
20 | %runElab deriveJSON defaultOpts `{HoverClientCapabilities}
21 |
22 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
23 | public export
24 | record HoverOptions where
25 |   constructor MkHoverOptions
26 |   workDoneProgress : Maybe Bool
27 | %runElab deriveJSON defaultOpts `{HoverOptions}
28 |
29 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
30 | public export
31 | record HoverRegistrationOptions where
32 |   constructor MkHoverRegistrationOptions
33 |   workDoneProgress : Maybe Bool
34 |   documentSelector : OneOf [DocumentSelector, Null]
35 | %runElab deriveJSON defaultOpts `{HoverRegistrationOptions}
36 |
37 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
38 | public export
39 | record HoverParams where
40 |   constructor MkHoverParams
41 |   workDoneToken : Maybe ProgressToken
42 |   textDocument : TextDocumentIdentifier
43 |   position : Position
44 | %runElab deriveJSON defaultOpts `{HoverParams}
45 |
46 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
47 | public export
48 | record Hover where
49 |   constructor MkHover
50 |   contents : OneOf [MarkedString, List MarkedString, MarkupContent]
51 |   range : Maybe Range
52 | %runElab deriveJSON defaultOpts `{Hover}
53 |