0 | module Language.LSP.Message.TextDocument
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.Derive
  4 | import Language.LSP.Message.Location
  5 | import Language.LSP.Message.URI
  6 | import Language.LSP.Message.Utils
  7 | import Language.Reflection
  8 |
  9 | %language ElabReflection
 10 | %default total
 11 |
 12 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentIdentifier
 13 | public export
 14 | record TextDocumentIdentifier where
 15 |   constructor MkTextDocumentIdentifier
 16 |   uri : DocumentURI
 17 | %runElab deriveJSON defaultOpts `{TextDocumentIdentifier}
 18 |
 19 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier
 20 | public export
 21 | record VersionedTextDocumentIdentifier where
 22 |   constructor MkVersionedTextDocumentIdentifier
 23 |   uri     : DocumentURI
 24 |   version : Int
 25 | %runElab deriveJSON defaultOpts `{VersionedTextDocumentIdentifier}
 26 |
 27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier
 28 | public export
 29 | record OptionalVersionedTextDocumentIdentifier where
 30 |   constructor MkOptionalVersionedTextDocumentIdentifier
 31 |   uri     : DocumentURI
 32 |   version : Maybe Int
 33 | %runElab deriveJSON defaultOpts `{OptionalVersionedTextDocumentIdentifier}
 34 |
 35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentItem
 36 | public export
 37 | record TextDocumentItem where
 38 |   constructor MkTextDocumentItem
 39 |   uri        : DocumentURI
 40 |   languageId : String
 41 |   version    : Int
 42 |   text       : String
 43 | %runElab deriveJSON defaultOpts `{TextDocumentItem}
 44 |
 45 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentPositionParams
 46 | public export
 47 | record TextDocumentPositionParams where
 48 |   constructor MkTextDocumentPositionParams
 49 |   textDocument : TextDocumentIdentifier
 50 |   position     : Position
 51 | %runElab deriveJSON defaultOpts `{TextDocumentPositionParams}
 52 |
 53 | namespace TextDocumentSyncKind
 54 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_synchronization
 55 |   public export
 56 |   data TextDocumentSyncKind = None | Full | Incremental
 57 |
 58 | export
 59 | ToJSON TextDocumentSyncKind where
 60 |   toJSON None        = JNumber 0
 61 |   toJSON Full        = JNumber 1
 62 |   toJSON Incremental = JNumber 2
 63 |
 64 | export
 65 | FromJSON TextDocumentSyncKind where
 66 |   fromJSON (JNumber 0) = pure None
 67 |   fromJSON (JNumber 1) = pure Full
 68 |   fromJSON (JNumber 2) = pure Incremental
 69 |   fromJSON _ = Nothing
 70 |
 71 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didOpen
 72 | public export
 73 | record DidOpenTextDocumentParams where
 74 |   constructor MkDidOpenTextDocumentParams
 75 |   textDocument : TextDocumentItem
 76 | %runElab deriveJSON defaultOpts `{DidOpenTextDocumentParams}
 77 |
 78 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter
 79 | public export
 80 | record DocumentFilter where
 81 |   constructor MkDocumentFilter
 82 |   language : Maybe String
 83 |   scheme   : Maybe String
 84 |   pattern  : Maybe String
 85 | %runElab deriveJSON defaultOpts `{DocumentFilter}
 86 |
 87 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter
 88 | public export
 89 | DocumentSelector : Type
 90 | DocumentSelector = List DocumentFilter
 91 |
 92 | public export
 93 | record TextDocumentRegistrationOptions where
 94 |   constructor MkTextDocumentRegistrationOptions
 95 |   documentSelector : OneOf [DocumentSelector, Null]
 96 | %runElab deriveJSON defaultOpts `{TextDocumentRegistrationOptions}
 97 |
 98 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentRegistrationOptions
 99 | public export
100 | record TextDocumentChangeRegistrationOptions where
101 |   constructor MkTextDocumentChangeRegistrationOptions
102 |   syncKind : TextDocumentSyncKind
103 | %runElab deriveJSON defaultOpts `{TextDocumentChangeRegistrationOptions}
104 |
105 | namespace DidChangeTextDocumentParams
106 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange
107 |   public export
108 |   record TextDocumentContentChangeEvent where
109 |     constructor MkTextDocumentContentChangeEvent
110 |     text : String
111 |   %runElab deriveJSON defaultOpts `{TextDocumentContentChangeEvent}
112 |
113 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange
114 |   public export
115 |   record TextDocumentContentChangeEventWithRange where
116 |     constructor MkTextDocumentContentChangeEventWithRange
117 |     range       : Range
118 |     rangeLength : Maybe Int
119 |     text        : String
120 |   %runElab deriveJSON defaultOpts `{TextDocumentContentChangeEventWithRange}
121 |
122 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange
123 | public export
124 | record DidChangeTextDocumentParams where
125 |   constructor MkDidChangeTextDocumentParams
126 |   textDocument   : VersionedTextDocumentIdentifier
127 |   contentChanges : List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange])
128 | %runElab deriveJSON defaultOpts `{DidChangeTextDocumentParams}
129 |
130 | namespace TextDocumentSaveReason
131 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave
132 |   public export
133 |   data TextDocumentSaveReason = Manual | AfterDelay | FocusOut
134 |
135 | export
136 | ToJSON TextDocumentSaveReason where
137 |   toJSON Manual     = JNumber 1
138 |   toJSON AfterDelay = JNumber 2
139 |   toJSON FocusOut   = JNumber 3
140 |
141 | export
142 | FromJSON TextDocumentSaveReason where
143 |   fromJSON (JNumber 1) = pure Manual
144 |   fromJSON (JNumber 2) = pure AfterDelay
145 |   fromJSON (JNumber 3) = pure FocusOut
146 |   fromJSON _ = neutral
147 |
148 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave
149 | public export
150 | record WillSaveTextDocumentParams where
151 |   constructor MkWillSaveTextDocumentParams
152 |   textDocument : TextDocumentIdentifier
153 |   reason       : TextDocumentSaveReason
154 | %runElab deriveJSON defaultOpts `{WillSaveTextDocumentParams}
155 |
156 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave
157 | public export
158 | record SaveOptions where
159 |   constructor MkSaveOptions
160 |   includeText : Maybe Bool
161 | %runElab deriveJSON defaultOpts `{SaveOptions}
162 |
163 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave
164 | public export
165 | record TextDocumentSaveRegistrationOptions where
166 |   constructor MkTextDocumentSaveRegistrationOptions
167 |   documentSelector : OneOf [DocumentSelector, Null]
168 |   includeText      : Maybe Bool
169 | %runElab deriveJSON defaultOpts `{TextDocumentSaveRegistrationOptions}
170 |
171 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave
172 | public export
173 | record DidSaveTextDocumentParams where
174 |   constructor MkDidSaveTextDocumentParams
175 |   textDocument : TextDocumentIdentifier
176 |   text         : Maybe String
177 | %runElab deriveJSON defaultOpts `{DidSaveTextDocumentParams}
178 |
179 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose
180 | public export
181 | record DidCloseTextDocumentParams where
182 |   constructor MkDidCloseTextDocumentParams
183 |   textDocument : TextDocumentIdentifier
184 | %runElab deriveJSON defaultOpts `{DidCloseTextDocumentParams}
185 |
186 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose
187 | public export
188 | record TextDocumentSyncClientCapabilities where
189 |   constructor MkTextDocumentSyncClientCapabilities
190 |   dynamicRegistration : Maybe Bool
191 |   willSave            : Maybe Bool
192 |   willSaveWaitUntil   : Maybe Bool
193 |   didSave             : Maybe Bool
194 | %runElab deriveJSON defaultOpts `{TextDocumentSyncClientCapabilities}
195 |
196 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose
197 | public export
198 | record TextDocumentSyncOptions where
199 |   constructor MkTextDocumentSyncOptions
200 |   openClose         : Maybe Bool
201 |   change            : Maybe TextDocumentSyncKind
202 |   willSave          : Maybe Bool
203 |   willSaveWaitUntil : Maybe Bool
204 |   save              : Maybe (OneOf [Bool, SaveOptions])
205 | %runElab deriveJSON defaultOpts `{TextDocumentSyncOptions}
206 |