Idris2Doc : Language.LSP.Message.TextDocument

Language.LSP.Message.TextDocument

(source)
Definitions
record TextDocumentIdentifier : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentIdentifier

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentIdentifier : DocumentURI -> TextDocumentIdentifier

  Projection: 
.uri : TextDocumentIdentifier -> DocumentURI

  Hints:
  
FromJSON TextDocumentIdentifier
  
ToJSON TextDocumentIdentifier
.uri : TextDocumentIdentifier -> DocumentURI
  Totality: total
  Visibility: public export
uri : TextDocumentIdentifier -> DocumentURI
  Totality: total
  Visibility: public export
record VersionedTextDocumentIdentifier : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier

  Totality: total
  Visibility: public export
  Constructor: 
MkVersionedTextDocumentIdentifier : DocumentURI -> Int -> VersionedTextDocumentIdentifier

  Projections:
  
.uri : VersionedTextDocumentIdentifier -> DocumentURI
  
.version : VersionedTextDocumentIdentifier -> Int

  Hints:
  
FromJSON VersionedTextDocumentIdentifier
  
ToJSON VersionedTextDocumentIdentifier
.uri : VersionedTextDocumentIdentifier -> DocumentURI
  Totality: total
  Visibility: public export
uri : VersionedTextDocumentIdentifier -> DocumentURI
  Totality: total
  Visibility: public export
.version : VersionedTextDocumentIdentifier -> Int
  Totality: total
  Visibility: public export
version : VersionedTextDocumentIdentifier -> Int
  Totality: total
  Visibility: public export
record OptionalVersionedTextDocumentIdentifier : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier

  Totality: total
  Visibility: public export
  Constructor: 
MkOptionalVersionedTextDocumentIdentifier : DocumentURI -> Maybe Int -> OptionalVersionedTextDocumentIdentifier

  Projections:
  
.uri : OptionalVersionedTextDocumentIdentifier -> DocumentURI
  
.version : OptionalVersionedTextDocumentIdentifier -> Maybe Int

  Hints:
  
FromJSON OptionalVersionedTextDocumentIdentifier
  
ToJSON OptionalVersionedTextDocumentIdentifier
.uri : OptionalVersionedTextDocumentIdentifier -> DocumentURI
  Totality: total
  Visibility: public export
uri : OptionalVersionedTextDocumentIdentifier -> DocumentURI
  Totality: total
  Visibility: public export
.version : OptionalVersionedTextDocumentIdentifier -> Maybe Int
  Totality: total
  Visibility: public export
version : OptionalVersionedTextDocumentIdentifier -> Maybe Int
  Totality: total
  Visibility: public export
record TextDocumentItem : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentItem

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentItem : DocumentURI -> String -> Int -> String -> TextDocumentItem

  Projections:
  
.languageId : TextDocumentItem -> String
  
.text : TextDocumentItem -> String
  
.uri : TextDocumentItem -> DocumentURI
  
.version : TextDocumentItem -> Int

  Hints:
  
FromJSON TextDocumentItem
  
ToJSON TextDocumentItem
.uri : TextDocumentItem -> DocumentURI
  Totality: total
  Visibility: public export
uri : TextDocumentItem -> DocumentURI
  Totality: total
  Visibility: public export
.languageId : TextDocumentItem -> String
  Totality: total
  Visibility: public export
languageId : TextDocumentItem -> String
  Totality: total
  Visibility: public export
.version : TextDocumentItem -> Int
  Totality: total
  Visibility: public export
version : TextDocumentItem -> Int
  Totality: total
  Visibility: public export
.text : TextDocumentItem -> String
  Totality: total
  Visibility: public export
text : TextDocumentItem -> String
  Totality: total
  Visibility: public export
record TextDocumentPositionParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentPositionParams

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentPositionParams : TextDocumentIdentifier -> Position -> TextDocumentPositionParams

  Projections:
  
.position : TextDocumentPositionParams -> Position
  
.textDocument : TextDocumentPositionParams -> TextDocumentIdentifier

  Hints:
  
FromJSON TextDocumentPositionParams
  
ToJSON TextDocumentPositionParams
.textDocument : TextDocumentPositionParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : TextDocumentPositionParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
.position : TextDocumentPositionParams -> Position
  Totality: total
  Visibility: public export
position : TextDocumentPositionParams -> Position
  Totality: total
  Visibility: public export
data TextDocumentSyncKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_synchronization

  Totality: total
  Visibility: public export
  Constructors:
  
None : TextDocumentSyncKind
  
Full : TextDocumentSyncKind
  
Incremental : TextDocumentSyncKind

  Hints:
  
FromJSON TextDocumentSyncKind
  
ToJSON TextDocumentSyncKind
record DidOpenTextDocumentParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didOpen

  Totality: total
  Visibility: public export
  Constructor: 
MkDidOpenTextDocumentParams : TextDocumentItem -> DidOpenTextDocumentParams

  Projection: 
.textDocument : DidOpenTextDocumentParams -> TextDocumentItem

  Hints:
  
FromJSON DidOpenTextDocumentParams
  
ToJSON DidOpenTextDocumentParams
.textDocument : DidOpenTextDocumentParams -> TextDocumentItem
  Totality: total
  Visibility: public export
textDocument : DidOpenTextDocumentParams -> TextDocumentItem
  Totality: total
  Visibility: public export
record DocumentFilter : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentFilter : Maybe String -> Maybe String -> Maybe String -> DocumentFilter

  Projections:
  
.language : DocumentFilter -> Maybe String
  
.pattern : DocumentFilter -> Maybe String
  
.scheme : DocumentFilter -> Maybe String

  Hints:
  
FromJSON DocumentFilter
  
ToJSON DocumentFilter
.language : DocumentFilter -> Maybe String
  Totality: total
  Visibility: public export
language : DocumentFilter -> Maybe String
  Totality: total
  Visibility: public export
.scheme : DocumentFilter -> Maybe String
  Totality: total
  Visibility: public export
scheme : DocumentFilter -> Maybe String
  Totality: total
  Visibility: public export
.pattern : DocumentFilter -> Maybe String
  Totality: total
  Visibility: public export
pattern : DocumentFilter -> Maybe String
  Totality: total
  Visibility: public export
DocumentSelector : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter

  Totality: total
  Visibility: public export
record TextDocumentRegistrationOptions : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentRegistrationOptions : OneOf [DocumentSelector, Null] -> TextDocumentRegistrationOptions

  Projection: 
.documentSelector : TextDocumentRegistrationOptions -> OneOf [DocumentSelector, Null]

  Hints:
  
FromJSON TextDocumentRegistrationOptions
  
ToJSON TextDocumentRegistrationOptions
.documentSelector : TextDocumentRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
documentSelector : TextDocumentRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
record TextDocumentChangeRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentRegistrationOptions

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentChangeRegistrationOptions : TextDocumentSyncKind -> TextDocumentChangeRegistrationOptions

  Projection: 
.syncKind : TextDocumentChangeRegistrationOptions -> TextDocumentSyncKind

  Hints:
  
FromJSON TextDocumentChangeRegistrationOptions
  
ToJSON TextDocumentChangeRegistrationOptions
.syncKind : TextDocumentChangeRegistrationOptions -> TextDocumentSyncKind
  Totality: total
  Visibility: public export
syncKind : TextDocumentChangeRegistrationOptions -> TextDocumentSyncKind
  Totality: total
  Visibility: public export
record TextDocumentContentChangeEvent : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentContentChangeEvent : String -> TextDocumentContentChangeEvent

  Projection: 
.text : TextDocumentContentChangeEvent -> String

  Hints:
  
FromJSON TextDocumentContentChangeEvent
  
ToJSON TextDocumentContentChangeEvent
.text : TextDocumentContentChangeEvent -> String
  Totality: total
  Visibility: public export
text : TextDocumentContentChangeEvent -> String
  Totality: total
  Visibility: public export
record TextDocumentContentChangeEventWithRange : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentContentChangeEventWithRange : Range -> Maybe Int -> String -> TextDocumentContentChangeEventWithRange

  Projections:
  
.range : TextDocumentContentChangeEventWithRange -> Range
  
.rangeLength : TextDocumentContentChangeEventWithRange -> Maybe Int
  
.text : TextDocumentContentChangeEventWithRange -> String

  Hints:
  
FromJSON TextDocumentContentChangeEventWithRange
  
ToJSON TextDocumentContentChangeEventWithRange
.range : TextDocumentContentChangeEventWithRange -> Range
  Totality: total
  Visibility: public export
range : TextDocumentContentChangeEventWithRange -> Range
  Totality: total
  Visibility: public export
.rangeLength : TextDocumentContentChangeEventWithRange -> Maybe Int
  Totality: total
  Visibility: public export
rangeLength : TextDocumentContentChangeEventWithRange -> Maybe Int
  Totality: total
  Visibility: public export
.text : TextDocumentContentChangeEventWithRange -> String
  Totality: total
  Visibility: public export
text : TextDocumentContentChangeEventWithRange -> String
  Totality: total
  Visibility: public export
record DidChangeTextDocumentParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeTextDocumentParams : VersionedTextDocumentIdentifier -> List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange]) -> DidChangeTextDocumentParams

  Projections:
  
.contentChanges : DidChangeTextDocumentParams -> List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange])
  
.textDocument : DidChangeTextDocumentParams -> VersionedTextDocumentIdentifier

  Hints:
  
FromJSON DidChangeTextDocumentParams
  
ToJSON DidChangeTextDocumentParams
.textDocument : DidChangeTextDocumentParams -> VersionedTextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : DidChangeTextDocumentParams -> VersionedTextDocumentIdentifier
  Totality: total
  Visibility: public export
.contentChanges : DidChangeTextDocumentParams -> List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange])
  Totality: total
  Visibility: public export
contentChanges : DidChangeTextDocumentParams -> List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange])
  Totality: total
  Visibility: public export
data TextDocumentSaveReason : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave

  Totality: total
  Visibility: public export
  Constructors:
  
Manual : TextDocumentSaveReason
  
AfterDelay : TextDocumentSaveReason
  
FocusOut : TextDocumentSaveReason

  Hints:
  
FromJSON TextDocumentSaveReason
  
ToJSON TextDocumentSaveReason
record WillSaveTextDocumentParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave

  Totality: total
  Visibility: public export
  Constructor: 
MkWillSaveTextDocumentParams : TextDocumentIdentifier -> TextDocumentSaveReason -> WillSaveTextDocumentParams

  Projections:
  
.reason : WillSaveTextDocumentParams -> TextDocumentSaveReason
  
.textDocument : WillSaveTextDocumentParams -> TextDocumentIdentifier

  Hints:
  
FromJSON WillSaveTextDocumentParams
  
ToJSON WillSaveTextDocumentParams
.textDocument : WillSaveTextDocumentParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : WillSaveTextDocumentParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
.reason : WillSaveTextDocumentParams -> TextDocumentSaveReason
  Totality: total
  Visibility: public export
reason : WillSaveTextDocumentParams -> TextDocumentSaveReason
  Totality: total
  Visibility: public export
record SaveOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave

  Totality: total
  Visibility: public export
  Constructor: 
MkSaveOptions : Maybe Bool -> SaveOptions

  Projection: 
.includeText : SaveOptions -> Maybe Bool

  Hints:
  
FromJSON SaveOptions
  
ToJSON SaveOptions
.includeText : SaveOptions -> Maybe Bool
  Totality: total
  Visibility: public export
includeText : SaveOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record TextDocumentSaveRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentSaveRegistrationOptions : OneOf [DocumentSelector, Null] -> Maybe Bool -> TextDocumentSaveRegistrationOptions

  Projections:
  
.documentSelector : TextDocumentSaveRegistrationOptions -> OneOf [DocumentSelector, Null]
  
.includeText : TextDocumentSaveRegistrationOptions -> Maybe Bool

  Hints:
  
FromJSON TextDocumentSaveRegistrationOptions
  
ToJSON TextDocumentSaveRegistrationOptions
.documentSelector : TextDocumentSaveRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
documentSelector : TextDocumentSaveRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
.includeText : TextDocumentSaveRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
includeText : TextDocumentSaveRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record DidSaveTextDocumentParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave

  Totality: total
  Visibility: public export
  Constructor: 
MkDidSaveTextDocumentParams : TextDocumentIdentifier -> Maybe String -> DidSaveTextDocumentParams

  Projections:
  
.text : DidSaveTextDocumentParams -> Maybe String
  
.textDocument : DidSaveTextDocumentParams -> TextDocumentIdentifier

  Hints:
  
FromJSON DidSaveTextDocumentParams
  
ToJSON DidSaveTextDocumentParams
.textDocument : DidSaveTextDocumentParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : DidSaveTextDocumentParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
.text : DidSaveTextDocumentParams -> Maybe String
  Totality: total
  Visibility: public export
text : DidSaveTextDocumentParams -> Maybe String
  Totality: total
  Visibility: public export
record DidCloseTextDocumentParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose

  Totality: total
  Visibility: public export
  Constructor: 
MkDidCloseTextDocumentParams : TextDocumentIdentifier -> DidCloseTextDocumentParams

  Projection: 
.textDocument : DidCloseTextDocumentParams -> TextDocumentIdentifier

  Hints:
  
FromJSON DidCloseTextDocumentParams
  
ToJSON DidCloseTextDocumentParams
.textDocument : DidCloseTextDocumentParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : DidCloseTextDocumentParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
record TextDocumentSyncClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentSyncClientCapabilities : Maybe Bool -> Maybe Bool -> Maybe Bool -> Maybe Bool -> TextDocumentSyncClientCapabilities

  Projections:
  
.didSave : TextDocumentSyncClientCapabilities -> Maybe Bool
  
.dynamicRegistration : TextDocumentSyncClientCapabilities -> Maybe Bool
  
.willSave : TextDocumentSyncClientCapabilities -> Maybe Bool
  
.willSaveWaitUntil : TextDocumentSyncClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON TextDocumentSyncClientCapabilities
  
ToJSON TextDocumentSyncClientCapabilities
.dynamicRegistration : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.willSave : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
willSave : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.willSaveWaitUntil : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
willSaveWaitUntil : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.didSave : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
didSave : TextDocumentSyncClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
record TextDocumentSyncOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentSyncOptions : Maybe Bool -> Maybe TextDocumentSyncKind -> Maybe Bool -> Maybe Bool -> Maybe (OneOf [Bool, SaveOptions]) -> TextDocumentSyncOptions

  Projections:
  
.change : TextDocumentSyncOptions -> Maybe TextDocumentSyncKind
  
.openClose : TextDocumentSyncOptions -> Maybe Bool
  
.save : TextDocumentSyncOptions -> Maybe (OneOf [Bool, SaveOptions])
  
.willSave : TextDocumentSyncOptions -> Maybe Bool
  
.willSaveWaitUntil : TextDocumentSyncOptions -> Maybe Bool

  Hints:
  
FromJSON TextDocumentSyncOptions
  
ToJSON TextDocumentSyncOptions
.openClose : TextDocumentSyncOptions -> Maybe Bool
  Totality: total
  Visibility: public export
openClose : TextDocumentSyncOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.change : TextDocumentSyncOptions -> Maybe TextDocumentSyncKind
  Totality: total
  Visibility: public export
change : TextDocumentSyncOptions -> Maybe TextDocumentSyncKind
  Totality: total
  Visibility: public export
.willSave : TextDocumentSyncOptions -> Maybe Bool
  Totality: total
  Visibility: public export
willSave : TextDocumentSyncOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.willSaveWaitUntil : TextDocumentSyncOptions -> Maybe Bool
  Totality: total
  Visibility: public export
willSaveWaitUntil : TextDocumentSyncOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.save : TextDocumentSyncOptions -> Maybe (OneOf [Bool, SaveOptions])
  Totality: total
  Visibility: public export
save : TextDocumentSyncOptions -> Maybe (OneOf [Bool, SaveOptions])
  Totality: total
  Visibility: public export