0 | module Language.LSP.Message.Moniker
 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 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
14 | public export
15 | record MonikerClientCapabilities where
16 |   constructor MkMonikerClientCapabilities
17 |   dynamicRegistration : Maybe Bool
18 | %runElab deriveJSON defaultOpts `{MonikerClientCapabilities}
19 |
20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
21 | public export
22 | record MonikerOptions where
23 |   constructor MkMonikersOptions
24 |   workDoneProgress : Maybe Bool
25 | %runElab deriveJSON defaultOpts `{MonikerOptions}
26 |
27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
28 | public export
29 | record MonikerRegistrationOptions where
30 |   constructor MkMonikersRegistrationOptions
31 |   workDoneProgress : Maybe Bool
32 |   documentSelector : OneOf [DocumentSelector, Null]
33 | %runElab deriveJSON defaultOpts `{MonikerRegistrationOptions}
34 |
35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
36 | public export
37 | record MonikerParams where
38 |   constructor MkMonikersParams
39 |   workDoneToken      : Maybe ProgressToken
40 |   partialResultToken : Maybe ProgressToken
41 |   textDocument       : TextDocumentIdentifier
42 |   position           : Position
43 | %runElab deriveJSON defaultOpts `{MonikerParams}
44 |
45 | namespace UniquenessLevel
46 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
47 |   public export
48 |   data UniquenessLevel = Document | Project | Group | Scheme | Global
49 |
50 | export
51 | ToJSON UniquenessLevel where
52 |   toJSON Document = JString "document"
53 |   toJSON Project = JString "project"
54 |   toJSON Group = JString "group"
55 |   toJSON Scheme = JString "scheme"
56 |   toJSON Global = JString "global"
57 |
58 | export
59 | FromJSON UniquenessLevel where
60 |   fromJSON (JString "document") = pure Document
61 |   fromJSON (JString "project") = pure Project
62 |   fromJSON (JString "group") = pure Group
63 |   fromJSON (JString "scheme") = pure Scheme
64 |   fromJSON (JString "global") = pure Global
65 |   fromJSON _ = neutral
66 |
67 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
68 | namespace MonikerKind
69 |   public export
70 |   data MonikerKind = Import | Export | Local
71 |
72 | export
73 | ToJSON MonikerKind where
74 |   toJSON Import = JString "import"
75 |   toJSON Export = JString "export"
76 |   toJSON Local  = JString "local"
77 |
78 | export
79 | FromJSON MonikerKind where
80 |   fromJSON (JString "import") = pure Import
81 |   fromJSON (JString "export") = pure Export
82 |   fromJSON (JString "local")  = pure Local
83 |   fromJSON _ = neutral
84 |
85 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
86 | public export
87 | record Moniker where
88 |   constructor MkMoniker
89 |   scheme     : String
90 |   identifier : String
91 |   unique     : UniquenessLevel
92 |   kind       : Maybe MonikerKind
93 | %runElab deriveJSON defaultOpts `{Moniker}
94 |