0 | module Language.LSP.Message.SemanticTokens
  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 SemanticTokenClientCapabilities
 14 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 15 |   public export
 16 |   record SemanticTokenRequestsFull where
 17 |     constructor MkSemanticTokenRequestsFull
 18 |     delta : Maybe Bool
 19 |   %runElab deriveJSON defaultOpts `{SemanticTokenRequestsFull}
 20 |
 21 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 22 |   public export
 23 |   record SemanticTokenRequests where
 24 |     constructor MkSemanticTokenRequests
 25 |     range : Maybe (OneOf [Bool, ()])
 26 |     full  : Maybe (OneOf [Bool, SemanticTokenRequestsFull])
 27 |   %runElab deriveJSON defaultOpts `{SemanticTokenRequests}
 28 |
 29 | namespace TokenFormat
 30 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 31 |   public export
 32 |   data TokenFormat = Relative
 33 |
 34 | export
 35 | ToJSON TokenFormat where
 36 |   toJSON Relative = JString "relative"
 37 |
 38 | export
 39 | FromJSON TokenFormat where
 40 |   fromJSON (JString "relative") = pure Relative
 41 |   fromJSON _ = neutral
 42 |
 43 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 44 | public export
 45 | record SemanticTokensLegend where
 46 |   constructor MkSemanticTokensLegend
 47 |   tokenTypes     : List String
 48 |   tokenModifiers : List String
 49 | %runElab deriveJSON defaultOpts `{SemanticTokensLegend}
 50 |
 51 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 52 | public export
 53 | record SemanticTokensClientCapabilities where
 54 |   constructor MkSemanticTokensClientCapabilities
 55 |   dynamicRegistration     : Maybe Bool
 56 |   requests                : SemanticTokenRequests
 57 |   tokenTypes              : List String
 58 |   tokenModifiers          : List String
 59 |   formats                 : List TokenFormat
 60 |   overlappingTokenSupport : Maybe Bool
 61 |   multilineTokenSupport   : Maybe Bool
 62 | %runElab deriveJSON defaultOpts `{SemanticTokensClientCapabilities}
 63 |
 64 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 65 | public export
 66 | record SemanticTokensOptions where
 67 |   constructor MkSemanticTokensOptions
 68 |   legend : SemanticTokensLegend
 69 |   range  : Maybe (OneOf [Bool, ()])
 70 |   full   : Maybe (OneOf [Bool, SemanticTokenRequestsFull])
 71 | %runElab deriveJSON defaultOpts `{SemanticTokensOptions}
 72 |
 73 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 74 | public export
 75 | record SemanticTokensRegistrationOptions where
 76 |   constructor MkSemanticTokensRegistrationOptions
 77 |   legend           : SemanticTokensLegend
 78 |   range            : Maybe (OneOf [Bool, ()])
 79 |   full             : Maybe (OneOf [Bool, SemanticTokenRequestsFull])
 80 |   documentSelector : OneOf [DocumentSelector, Null]
 81 |   id               : Maybe Bool
 82 | %runElab deriveJSON defaultOpts `{SemanticTokensRegistrationOptions}
 83 |
 84 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 85 | public export
 86 | record SemanticTokensParams where
 87 |   constructor MkSemanticTokensParams
 88 |   workDoneToken      : Maybe ProgressToken
 89 |   partialResultToken : Maybe ProgressToken
 90 |   textDocument       : TextDocumentIdentifier
 91 | %runElab deriveJSON defaultOpts `{SemanticTokensParams}
 92 |
 93 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
 94 | public export
 95 | record SemanticTokens where
 96 |   constructor MkSemanticTokens
 97 |   resultId : Maybe String
 98 |   data_    : List Int
 99 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{SemanticTokens}
100 |
101 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
102 | public export
103 | record SemanticTokensPartialResult where
104 |   constructor MkSemanticTokensPartialResult
105 |   data_ : List Int
106 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{SemanticTokensPartialResult}
107 |
108 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
109 | public export
110 | record SemanticTokensDeltaParams where
111 |   constructor MkSemanticTokensDeltaParams
112 |   workDoneToken      : Maybe ProgressToken
113 |   partialResultToken : Maybe ProgressToken
114 |   textDocument       : TextDocumentIdentifier
115 |   previousResultId   : String
116 | %runElab deriveJSON defaultOpts `{SemanticTokensDeltaParams}
117 |
118 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
119 | public export
120 | record SemanticTokensEdit where
121 |   constructor MkSemanticTokensEdit
122 |   start       : Int
123 |   deleteCount : Int
124 |   data_       : Maybe (List Int)
125 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{SemanticTokensEdit}
126 |
127 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
128 | public export
129 | record SemanticTokensDelta where
130 |   constructor MkSemanticTokensDelta
131 |   resultId : Maybe String
132 |   edits    : List SemanticTokensEdit
133 | %runElab deriveJSON defaultOpts `{SemanticTokensDelta}
134 |
135 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
136 | public export
137 | record SemanticTokensDeltaPartialResult where
138 |   constructor MkSemanticTokensDeltaPartialResult
139 |   edits : List SemanticTokensEdit
140 | %runElab deriveJSON defaultOpts `{SemanticTokensDeltaPartialResult}
141 |
142 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
143 | public export
144 | record SemanticTokensRangeParams where
145 |   constructor MkSemanticTokensRangeParams
146 |   workDoneToken      : Maybe ProgressToken
147 |   partialResultToken : Maybe ProgressToken
148 |   textDocument       : TextDocumentIdentifier
149 |   range              : Range
150 | %runElab deriveJSON defaultOpts `{SemanticTokensRangeParams}
151 |
152 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
153 | public export
154 | record SemanticTokensWorkspaceClientCapabilities where
155 |   constructor MkSemanticTokensWorkspaceClientCapabilities
156 |   refreshSupport : Maybe Bool
157 | %runElab deriveJSON defaultOpts `{SemanticTokensWorkspaceClientCapabilities}
158 |