
  0 | module Language.LSP.Message.References
  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_references
 14 | public export
 15 | record ReferenceClientCapabilities where
 16 |   constructor MkReferenceClientCapabilities
 17 |   dynamicRegistration : Maybe Bool
 18 | %runElab deriveJSON defaultOpts `{ReferenceClientCapabilities}
 19 | 
 20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references
 21 | public export
 22 | record ReferenceOptions where
 23 |   constructor MkReferenceOptions
 24 |   workDoneProgress : Maybe Bool
 25 | %runElab deriveJSON defaultOpts `{ReferenceOptions}
 26 | 
 27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references
 28 | public export
 29 | record ReferenceRegistrationOptions where
 30 |   constructor MkReferenceRegistrationOptions
 31 |   workDoneProgress : Maybe Bool
 32 |   documentSelector : OneOf [DocumentSelector, Null]
 33 | %runElab deriveJSON defaultOpts `{ReferenceRegistrationOptions}
 34 | 
 35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references
 36 | public export
 37 | record ReferenceContext where
 38 |   constructor MkReferenceContext
 39 |   includeDeclaration : Bool
 40 | %runElab deriveJSON defaultOpts `{ReferenceContext}
 41 | 
 42 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references
 43 | public export
 44 | record ReferenceParams where
 45 |   constructor MkReferenceParams
 46 |   workDoneToken      : Maybe ProgressToken
 47 |   partialResultToken : Maybe ProgressToken
 48 |   textDocument       : TextDocumentIdentifier
 49 |   position           : Position
 50 |   context            : ReferenceContext
 51 | %runElab deriveJSON defaultOpts `{ReferenceParams}
 52 |