Idris2Doc : Language.LSP.Message.Workspace

Language.LSP.Message.Workspace

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

  Totality: total
  Visibility: public export
  Constructor: 
MkTextEdit : Range -> String -> TextEdit

  Projections:
  
.newText : TextEdit -> String
  
.range : TextEdit -> Range

  Hints:
  
Eq TextEdit
  
FromJSON TextEdit
  
ToJSON TextEdit
.range : TextEdit -> Range
  Totality: total
  Visibility: public export
range : TextEdit -> Range
  Totality: total
  Visibility: public export
.newText : TextEdit -> String
  Totality: total
  Visibility: public export
newText : TextEdit -> String
  Totality: total
  Visibility: public export
record ChangeAnnotation : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit

  Totality: total
  Visibility: public export
  Constructor: 
MkChangeAnnotation : String -> Maybe Bool -> Maybe String -> ChangeAnnotation

  Projections:
  
.description : ChangeAnnotation -> Maybe String
  
.label : ChangeAnnotation -> String
  
.needsConfirmation : ChangeAnnotation -> Maybe Bool

  Hints:
  
FromJSON ChangeAnnotation
  
ToJSON ChangeAnnotation
.label : ChangeAnnotation -> String
  Totality: total
  Visibility: public export
label : ChangeAnnotation -> String
  Totality: total
  Visibility: public export
.needsConfirmation : ChangeAnnotation -> Maybe Bool
  Totality: total
  Visibility: public export
needsConfirmation : ChangeAnnotation -> Maybe Bool
  Totality: total
  Visibility: public export
.description : ChangeAnnotation -> Maybe String
  Totality: total
  Visibility: public export
description : ChangeAnnotation -> Maybe String
  Totality: total
  Visibility: public export
ChangeAnnotationIdentifier : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit

  Totality: total
  Visibility: public export
record AnnotatedTextEdit : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit

  Totality: total
  Visibility: public export
  Constructor: 
MkAnnotatedTextEdit : Range -> String -> ChangeAnnotationIdentifier -> AnnotatedTextEdit

  Projections:
  
.annotationId : AnnotatedTextEdit -> ChangeAnnotationIdentifier
  
.newText : AnnotatedTextEdit -> String
  
.range : AnnotatedTextEdit -> Range

  Hints:
  
FromJSON AnnotatedTextEdit
  
ToJSON AnnotatedTextEdit
.range : AnnotatedTextEdit -> Range
  Totality: total
  Visibility: public export
range : AnnotatedTextEdit -> Range
  Totality: total
  Visibility: public export
.newText : AnnotatedTextEdit -> String
  Totality: total
  Visibility: public export
newText : AnnotatedTextEdit -> String
  Totality: total
  Visibility: public export
.annotationId : AnnotatedTextEdit -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
annotationId : AnnotatedTextEdit -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
record TextDocumentEdit : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentEdit

  Totality: total
  Visibility: public export
  Constructor: 
MkTextDocumentEdit : OptionalVersionedTextDocumentIdentifier -> List (OneOf [TextEdit, AnnotatedTextEdit]) -> TextDocumentEdit

  Projections:
  
.edits : TextDocumentEdit -> List (OneOf [TextEdit, AnnotatedTextEdit])
  
.textDocument : TextDocumentEdit -> OptionalVersionedTextDocumentIdentifier

  Hints:
  
FromJSON TextDocumentEdit
  
ToJSON TextDocumentEdit
.textDocument : TextDocumentEdit -> OptionalVersionedTextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : TextDocumentEdit -> OptionalVersionedTextDocumentIdentifier
  Totality: total
  Visibility: public export
.edits : TextDocumentEdit -> List (OneOf [TextEdit, AnnotatedTextEdit])
  Totality: total
  Visibility: public export
edits : TextDocumentEdit -> List (OneOf [TextEdit, AnnotatedTextEdit])
  Totality: total
  Visibility: public export
record InsertReplaceEdit : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion

  Totality: total
  Visibility: public export
  Constructor: 
MkInsertReplaceEdit : String -> Range -> Range -> InsertReplaceEdit

  Projections:
  
.insert : InsertReplaceEdit -> Range
  
.newText : InsertReplaceEdit -> String
  
.replace : InsertReplaceEdit -> Range

  Hints:
  
FromJSON InsertReplaceEdit
  
ToJSON InsertReplaceEdit
.newText : InsertReplaceEdit -> String
  Totality: total
  Visibility: public export
newText : InsertReplaceEdit -> String
  Totality: total
  Visibility: public export
.insert : InsertReplaceEdit -> Range
  Totality: total
  Visibility: public export
insert : InsertReplaceEdit -> Range
  Totality: total
  Visibility: public export
.replace : InsertReplaceEdit -> Range
  Totality: total
  Visibility: public export
replace : InsertReplaceEdit -> Range
  Totality: total
  Visibility: public export
record CreateFileOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges

  Totality: total
  Visibility: public export
  Constructor: 
MkCreateFileOptions : Maybe Bool -> Maybe Bool -> CreateFileOptions

  Projections:
  
.ignoreIfExists : CreateFileOptions -> Maybe Bool
  
.overwrite : CreateFileOptions -> Maybe Bool

  Hints:
  
FromJSON CreateFileOptions
  
ToJSON CreateFileOptions
.overwrite : CreateFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
overwrite : CreateFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.ignoreIfExists : CreateFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
ignoreIfExists : CreateFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record RenameFileOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges

  Totality: total
  Visibility: public export
  Constructor: 
MkRenameFileOptions : Maybe Bool -> Maybe Bool -> RenameFileOptions

  Projections:
  
.ignoreIfExists : RenameFileOptions -> Maybe Bool
  
.overwrite : RenameFileOptions -> Maybe Bool

  Hints:
  
FromJSON RenameFileOptions
  
ToJSON RenameFileOptions
.overwrite : RenameFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
overwrite : RenameFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.ignoreIfExists : RenameFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
ignoreIfExists : RenameFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record DeleteFileOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges

  Totality: total
  Visibility: public export
  Constructor: 
MkDeleteFileOptions : Maybe Bool -> Maybe Bool -> DeleteFileOptions

  Projections:
  
.ignoreIfNotExists : DeleteFileOptions -> Maybe Bool
  
.recursive : DeleteFileOptions -> Maybe Bool

  Hints:
  
FromJSON DeleteFileOptions
  
ToJSON DeleteFileOptions
.recursive : DeleteFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
recursive : DeleteFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.ignoreIfNotExists : DeleteFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
ignoreIfNotExists : DeleteFileOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record CreateFile : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges

  Totality: total
  Visibility: public export
  Constructor: 
MkCreateFile : DocumentURI -> Maybe CreateFileOptions -> ChangeAnnotationIdentifier -> CreateFile

  Projections:
  
.annotationId : CreateFile -> ChangeAnnotationIdentifier
  
.options : CreateFile -> Maybe CreateFileOptions
  
.uri : CreateFile -> DocumentURI

  Hints:
  
FromJSON CreateFile
  
ToJSON CreateFile
.uri : CreateFile -> DocumentURI
  Totality: total
  Visibility: public export
uri : CreateFile -> DocumentURI
  Totality: total
  Visibility: public export
.options : CreateFile -> Maybe CreateFileOptions
  Totality: total
  Visibility: public export
options : CreateFile -> Maybe CreateFileOptions
  Totality: total
  Visibility: public export
.annotationId : CreateFile -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
annotationId : CreateFile -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
record RenameFile : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges

  Totality: total
  Visibility: public export
  Constructor: 
MkRenameFile : DocumentURI -> DocumentURI -> Maybe RenameFileOptions -> ChangeAnnotationIdentifier -> RenameFile

  Projections:
  
.annotationId : RenameFile -> ChangeAnnotationIdentifier
  
.newUri : RenameFile -> DocumentURI
  
.oldUri : RenameFile -> DocumentURI
  
.options : RenameFile -> Maybe RenameFileOptions

  Hints:
  
FromJSON RenameFile
  
ToJSON RenameFile
.oldUri : RenameFile -> DocumentURI
  Totality: total
  Visibility: public export
oldUri : RenameFile -> DocumentURI
  Totality: total
  Visibility: public export
.newUri : RenameFile -> DocumentURI
  Totality: total
  Visibility: public export
newUri : RenameFile -> DocumentURI
  Totality: total
  Visibility: public export
.options : RenameFile -> Maybe RenameFileOptions
  Totality: total
  Visibility: public export
options : RenameFile -> Maybe RenameFileOptions
  Totality: total
  Visibility: public export
.annotationId : RenameFile -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
annotationId : RenameFile -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
record DeleteFile : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges

  Totality: total
  Visibility: public export
  Constructor: 
MkDeleteFile : DocumentURI -> Maybe DeleteFileOptions -> ChangeAnnotationIdentifier -> DeleteFile

  Projections:
  
.annotationId : DeleteFile -> ChangeAnnotationIdentifier
  
.options : DeleteFile -> Maybe DeleteFileOptions
  
.uri : DeleteFile -> DocumentURI

  Hints:
  
FromJSON DeleteFile
  
ToJSON DeleteFile
.uri : DeleteFile -> DocumentURI
  Totality: total
  Visibility: public export
uri : DeleteFile -> DocumentURI
  Totality: total
  Visibility: public export
.options : DeleteFile -> Maybe DeleteFileOptions
  Totality: total
  Visibility: public export
options : DeleteFile -> Maybe DeleteFileOptions
  Totality: total
  Visibility: public export
.annotationId : DeleteFile -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
annotationId : DeleteFile -> ChangeAnnotationIdentifier
  Totality: total
  Visibility: public export
record WorkspaceEdit : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEdit

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceEdit : Maybe (SortedMap DocumentURI (List TextEdit)) -> Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile])) -> Maybe (SortedMap String ChangeAnnotation) -> WorkspaceEdit

  Projections:
  
.changeAnnotations : WorkspaceEdit -> Maybe (SortedMap String ChangeAnnotation)
  
.changes : WorkspaceEdit -> Maybe (SortedMap DocumentURI (List TextEdit))
  
.documentChanges : WorkspaceEdit -> Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile]))

  Hints:
  
FromJSON WorkspaceEdit
  
ToJSON WorkspaceEdit
.changes : WorkspaceEdit -> Maybe (SortedMap DocumentURI (List TextEdit))
  Totality: total
  Visibility: public export
changes : WorkspaceEdit -> Maybe (SortedMap DocumentURI (List TextEdit))
  Totality: total
  Visibility: public export
.documentChanges : WorkspaceEdit -> Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile]))
  Totality: total
  Visibility: public export
documentChanges : WorkspaceEdit -> Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile]))
  Totality: total
  Visibility: public export
.changeAnnotations : WorkspaceEdit -> Maybe (SortedMap String ChangeAnnotation)
  Totality: total
  Visibility: public export
changeAnnotations : WorkspaceEdit -> Maybe (SortedMap String ChangeAnnotation)
  Totality: total
  Visibility: public export
data ResourceOperationKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities

  Totality: total
  Visibility: public export
  Constructors:
  
Create : ResourceOperationKind
  
Rename : ResourceOperationKind
  
Delete : ResourceOperationKind

  Hints:
  
FromJSON ResourceOperationKind
  
ToJSON ResourceOperationKind
data FailureHandlingKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities

  Totality: total
  Visibility: public export
  Constructors:
  
Abort : FailureHandlingKind
  
Transactional : FailureHandlingKind
  
Undo : FailureHandlingKind
  
TextOnlyTransactional : FailureHandlingKind

  Hints:
  
FromJSON FailureHandlingKind
  
ToJSON FailureHandlingKind
record ChangeAnnotationSupport : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities

  Totality: total
  Visibility: public export
  Constructor: 
MkChangeAnnotationSupport : Maybe Bool -> ChangeAnnotationSupport

  Projection: 
.groupsOnLabel : ChangeAnnotationSupport -> Maybe Bool

  Hints:
  
FromJSON ChangeAnnotationSupport
  
ToJSON ChangeAnnotationSupport
.groupsOnLabel : ChangeAnnotationSupport -> Maybe Bool
  Totality: total
  Visibility: public export
groupsOnLabel : ChangeAnnotationSupport -> Maybe Bool
  Totality: total
  Visibility: public export
record WorkspaceEditClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceEditClientCapabilities : Maybe Bool -> Maybe (List ResourceOperationKind) -> Maybe FailureHandlingKind -> Maybe Bool -> Maybe ChangeAnnotationSupport -> WorkspaceEditClientCapabilities

  Projections:
  
.changeAnnotationSupport : WorkspaceEditClientCapabilities -> Maybe ChangeAnnotationSupport
  
.documentChanges : WorkspaceEditClientCapabilities -> Maybe Bool
  
.failureHandling : WorkspaceEditClientCapabilities -> Maybe FailureHandlingKind
  
.normalizesLineEndings : WorkspaceEditClientCapabilities -> Maybe Bool
  
.resourceOperations : WorkspaceEditClientCapabilities -> Maybe (List ResourceOperationKind)

  Hints:
  
FromJSON WorkspaceEditClientCapabilities
  
ToJSON WorkspaceEditClientCapabilities
.documentChanges : WorkspaceEditClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
documentChanges : WorkspaceEditClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.resourceOperations : WorkspaceEditClientCapabilities -> Maybe (List ResourceOperationKind)
  Totality: total
  Visibility: public export
resourceOperations : WorkspaceEditClientCapabilities -> Maybe (List ResourceOperationKind)
  Totality: total
  Visibility: public export
.failureHandling : WorkspaceEditClientCapabilities -> Maybe FailureHandlingKind
  Totality: total
  Visibility: public export
failureHandling : WorkspaceEditClientCapabilities -> Maybe FailureHandlingKind
  Totality: total
  Visibility: public export
.normalizesLineEndings : WorkspaceEditClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
normalizesLineEndings : WorkspaceEditClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.changeAnnotationSupport : WorkspaceEditClientCapabilities -> Maybe ChangeAnnotationSupport
  Totality: total
  Visibility: public export
changeAnnotationSupport : WorkspaceEditClientCapabilities -> Maybe ChangeAnnotationSupport
  Totality: total
  Visibility: public export
record WorkspaceFoldersServerCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceFoldersServerCapabilities : Maybe Bool -> Maybe (OneOf [String, Bool]) -> WorkspaceFoldersServerCapabilities

  Projections:
  
.changeNotifications : WorkspaceFoldersServerCapabilities -> Maybe (OneOf [String, Bool])
  
.supported : WorkspaceFoldersServerCapabilities -> Maybe Bool

  Hints:
  
FromJSON WorkspaceFoldersServerCapabilities
  
ToJSON WorkspaceFoldersServerCapabilities
.supported : WorkspaceFoldersServerCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
supported : WorkspaceFoldersServerCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.changeNotifications : WorkspaceFoldersServerCapabilities -> Maybe (OneOf [String, Bool])
  Totality: total
  Visibility: public export
changeNotifications : WorkspaceFoldersServerCapabilities -> Maybe (OneOf [String, Bool])
  Totality: total
  Visibility: public export
record WorkspaceFolder : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceFolder : DocumentURI -> String -> WorkspaceFolder

  Projections:
  
.name : WorkspaceFolder -> String
  
.uri : WorkspaceFolder -> DocumentURI

  Hints:
  
FromJSON WorkspaceFolder
  
ToJSON WorkspaceFolder
.uri : WorkspaceFolder -> DocumentURI
  Totality: total
  Visibility: public export
uri : WorkspaceFolder -> DocumentURI
  Totality: total
  Visibility: public export
.name : WorkspaceFolder -> String
  Totality: total
  Visibility: public export
name : WorkspaceFolder -> String
  Totality: total
  Visibility: public export
interface WorkspaceFoldersChangeEvent : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders

  Methods:
  
added : List WorkspaceFolder
  
removed : List WorkspaceFolder
added : WorkspaceFoldersChangeEvent => List WorkspaceFolder
  Totality: total
  Visibility: public export
removed : WorkspaceFoldersChangeEvent => List WorkspaceFolder
  Totality: total
  Visibility: public export
record DidChangeWorkspaceFoldersParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeWorkspaceFoldersParams : WorkspaceFoldersChangeEvent -> DidChangeWorkspaceFoldersParams

  Projection: 
.event : DidChangeWorkspaceFoldersParams -> WorkspaceFoldersChangeEvent

  Hints:
  
FromJSON DidChangeWorkspaceFoldersParams
  
ToJSON DidChangeWorkspaceFoldersParams
.event : DidChangeWorkspaceFoldersParams -> WorkspaceFoldersChangeEvent
  Totality: total
  Visibility: public export
event : DidChangeWorkspaceFoldersParams -> WorkspaceFoldersChangeEvent
  Totality: total
  Visibility: public export
record DidChangeConfigurationClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeConfigurationClientCapabilities : Maybe Bool -> DidChangeConfigurationClientCapabilities

  Projection: 
.dynamicRegistration : DidChangeConfigurationClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON DidChangeConfigurationClientCapabilities
  
ToJSON DidChangeConfigurationClientCapabilities
.dynamicRegistration : DidChangeConfigurationClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : DidChangeConfigurationClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
record DidChangeConfigurationParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeConfigurationParams : JSON -> DidChangeConfigurationParams

  Projection: 
.settings : DidChangeConfigurationParams -> JSON

  Hints:
  
FromJSON DidChangeConfigurationParams
  
ToJSON DidChangeConfigurationParams
.settings : DidChangeConfigurationParams -> JSON
  Totality: total
  Visibility: public export
settings : DidChangeConfigurationParams -> JSON
  Totality: total
  Visibility: public export
record ConfigurationItem : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration

  Totality: total
  Visibility: public export
  Constructor: 
MkConfigurationItem : Maybe DocumentURI -> Maybe String -> ConfigurationItem

  Projections:
  
.scopeUri : ConfigurationItem -> Maybe DocumentURI
  
.section : ConfigurationItem -> Maybe String

  Hints:
  
FromJSON ConfigurationItem
  
ToJSON ConfigurationItem
.scopeUri : ConfigurationItem -> Maybe DocumentURI
  Totality: total
  Visibility: public export
scopeUri : ConfigurationItem -> Maybe DocumentURI
  Totality: total
  Visibility: public export
.section : ConfigurationItem -> Maybe String
  Totality: total
  Visibility: public export
section : ConfigurationItem -> Maybe String
  Totality: total
  Visibility: public export
record ConfigurationParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration

  Totality: total
  Visibility: public export
  Constructor: 
MkConfigurationParams : List ConfigurationItem -> ConfigurationParams

  Projection: 
.items : ConfigurationParams -> List ConfigurationItem

  Hints:
  
FromJSON ConfigurationParams
  
ToJSON ConfigurationParams
.items : ConfigurationParams -> List ConfigurationItem
  Totality: total
  Visibility: public export
items : ConfigurationParams -> List ConfigurationItem
  Totality: total
  Visibility: public export
record DidChangeWatchedFilesClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeWatchedFilesClientCapabilities : Maybe Bool -> DidChangeWatchedFilesClientCapabilities

  Projection: 
.dynamicRegistration : DidChangeWatchedFilesClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON DidChangeWatchedFilesClientCapabilities
  
ToJSON DidChangeWatchedFilesClientCapabilities
.dynamicRegistration : DidChangeWatchedFilesClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : DidChangeWatchedFilesClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
data WatchKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructors:
  
Create : WatchKind
  
Change : WatchKind
  
Delete : WatchKind

  Hints:
  
FromJSON (List WatchKind)
  
ToJSON (List WatchKind)
record FileSystemWatcher : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileSystemWatcher : String -> Maybe (List WatchKind) -> FileSystemWatcher

  Projections:
  
.globPattern : FileSystemWatcher -> String
  
.kind : FileSystemWatcher -> Maybe (List WatchKind)

  Hints:
  
FromJSON FileSystemWatcher
  
ToJSON FileSystemWatcher
.globPattern : FileSystemWatcher -> String
  Totality: total
  Visibility: public export
globPattern : FileSystemWatcher -> String
  Totality: total
  Visibility: public export
.kind : FileSystemWatcher -> Maybe (List WatchKind)
  Totality: total
  Visibility: public export
kind : FileSystemWatcher -> Maybe (List WatchKind)
  Totality: total
  Visibility: public export
record DidChangeWatchedFilesRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeWatchedFilesRegistrationOptions : List FileSystemWatcher -> DidChangeWatchedFilesRegistrationOptions

  Projection: 
.watchers : DidChangeWatchedFilesRegistrationOptions -> List FileSystemWatcher

  Hints:
  
FromJSON DidChangeWatchedFilesRegistrationOptions
  
ToJSON DidChangeWatchedFilesRegistrationOptions
.watchers : DidChangeWatchedFilesRegistrationOptions -> List FileSystemWatcher
  Totality: total
  Visibility: public export
watchers : DidChangeWatchedFilesRegistrationOptions -> List FileSystemWatcher
  Totality: total
  Visibility: public export
data FileChangeType : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructors:
  
Created : FileChangeType
  
Changed : FileChangeType
  
Deleted : FileChangeType

  Hints:
  
FromJSON FileChangeType
  
ToJSON FileChangeType
record FileEvent : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileEvent : DocumentURI -> FileChangeType -> FileEvent

  Projections:
  
.type : FileEvent -> FileChangeType
  
.uri : FileEvent -> DocumentURI

  Hints:
  
FromJSON FileEvent
  
ToJSON FileEvent
.uri : FileEvent -> DocumentURI
  Totality: total
  Visibility: public export
uri : FileEvent -> DocumentURI
  Totality: total
  Visibility: public export
.type : FileEvent -> FileChangeType
  Totality: total
  Visibility: public export
type : FileEvent -> FileChangeType
  Totality: total
  Visibility: public export
record DidChangeWatchedFilesParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkDidChangeWatchedFilesParams : List FileEvent -> DidChangeWatchedFilesParams

  Projection: 
.changes : DidChangeWatchedFilesParams -> List FileEvent

  Hints:
  
FromJSON DidChangeWatchedFilesParams
  
ToJSON DidChangeWatchedFilesParams
.changes : DidChangeWatchedFilesParams -> List FileEvent
  Totality: total
  Visibility: public export
changes : DidChangeWatchedFilesParams -> List FileEvent
  Totality: total
  Visibility: public export
record SymbolKindClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol

  Totality: total
  Visibility: public export
  Constructor: 
MkSymbolKindClientCapabilities : Maybe (List SymbolKind) -> SymbolKindClientCapabilities

  Projection: 
.valueSet : SymbolKindClientCapabilities -> Maybe (List SymbolKind)

  Hints:
  
FromJSON SymbolKindClientCapabilities
  
ToJSON SymbolKindClientCapabilities
.valueSet : SymbolKindClientCapabilities -> Maybe (List SymbolKind)
  Totality: total
  Visibility: public export
valueSet : SymbolKindClientCapabilities -> Maybe (List SymbolKind)
  Totality: total
  Visibility: public export
record TagSupportClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol

  Totality: total
  Visibility: public export
  Constructor: 
MkTagSupportClientCapabilities : List SymbolTag -> TagSupportClientCapabilities

  Projection: 
.valueSet : TagSupportClientCapabilities -> List SymbolTag

  Hints:
  
FromJSON TagSupportClientCapabilities
  
ToJSON TagSupportClientCapabilities
.valueSet : TagSupportClientCapabilities -> List SymbolTag
  Totality: total
  Visibility: public export
valueSet : TagSupportClientCapabilities -> List SymbolTag
  Totality: total
  Visibility: public export
record WorkspaceSymbolClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceSymbolClientCapabilities : Maybe Bool -> Maybe SymbolKindClientCapabilities -> TagSupportClientCapabilities -> WorkspaceSymbolClientCapabilities

  Projections:
  
.dynamicRegistration : WorkspaceSymbolClientCapabilities -> Maybe Bool
  
.symbolKind : WorkspaceSymbolClientCapabilities -> Maybe SymbolKindClientCapabilities
  
.tagSupport : WorkspaceSymbolClientCapabilities -> TagSupportClientCapabilities

  Hints:
  
FromJSON WorkspaceSymbolClientCapabilities
  
ToJSON WorkspaceSymbolClientCapabilities
.dynamicRegistration : WorkspaceSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : WorkspaceSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.symbolKind : WorkspaceSymbolClientCapabilities -> Maybe SymbolKindClientCapabilities
  Totality: total
  Visibility: public export
symbolKind : WorkspaceSymbolClientCapabilities -> Maybe SymbolKindClientCapabilities
  Totality: total
  Visibility: public export
.tagSupport : WorkspaceSymbolClientCapabilities -> TagSupportClientCapabilities
  Totality: total
  Visibility: public export
tagSupport : WorkspaceSymbolClientCapabilities -> TagSupportClientCapabilities
  Totality: total
  Visibility: public export
record WorkspaceSymbolOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceSymbolOptions : Maybe Bool -> WorkspaceSymbolOptions

  Projection: 
.workDoneProgress : WorkspaceSymbolOptions -> Maybe Bool

  Hints:
  
FromJSON WorkspaceSymbolOptions
  
ToJSON WorkspaceSymbolOptions
.workDoneProgress : WorkspaceSymbolOptions -> Maybe Bool
  Totality: total
  Visibility: public export
workDoneProgress : WorkspaceSymbolOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record WorkspaceSymbolRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceSymbolRegistrationOptions : Maybe Bool -> WorkspaceSymbolRegistrationOptions

  Projection: 
.workDoneProgress : WorkspaceSymbolRegistrationOptions -> Maybe Bool

  Hints:
  
FromJSON WorkspaceSymbolRegistrationOptions
  
ToJSON WorkspaceSymbolRegistrationOptions
.workDoneProgress : WorkspaceSymbolRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
workDoneProgress : WorkspaceSymbolRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record WorkspaceSymbolParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkspaceSymbolParams : Maybe ProgressToken -> String -> WorkspaceSymbolParams

  Projections:
  
.partialResultToken : WorkspaceSymbolParams -> Maybe ProgressToken
  
.query : WorkspaceSymbolParams -> String

  Hints:
  
FromJSON WorkspaceSymbolParams
  
ToJSON WorkspaceSymbolParams
.partialResultToken : WorkspaceSymbolParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : WorkspaceSymbolParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.query : WorkspaceSymbolParams -> String
  Totality: total
  Visibility: public export
query : WorkspaceSymbolParams -> String
  Totality: total
  Visibility: public export
record ApplyWorkspaceEditParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit

  Totality: total
  Visibility: public export
  Constructor: 
MkApplyWorkspaceEditParams : Maybe String -> WorkspaceEdit -> ApplyWorkspaceEditParams

  Projections:
  
.edit : ApplyWorkspaceEditParams -> WorkspaceEdit
  
.label : ApplyWorkspaceEditParams -> Maybe String

  Hints:
  
FromJSON ApplyWorkspaceEditParams
  
ToJSON ApplyWorkspaceEditParams
.label : ApplyWorkspaceEditParams -> Maybe String
  Totality: total
  Visibility: public export
label : ApplyWorkspaceEditParams -> Maybe String
  Totality: total
  Visibility: public export
.edit : ApplyWorkspaceEditParams -> WorkspaceEdit
  Totality: total
  Visibility: public export
edit : ApplyWorkspaceEditParams -> WorkspaceEdit
  Totality: total
  Visibility: public export
record ApplyWorkspaceEditResponse : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit

  Totality: total
  Visibility: public export
  Constructor: 
MkApplyWorkspaceEditResponse : Bool -> Maybe String -> Maybe Integer -> ApplyWorkspaceEditResponse

  Projections:
  
.applied : ApplyWorkspaceEditResponse -> Bool
  
.failedChange : ApplyWorkspaceEditResponse -> Maybe Integer
  
.failureReason : ApplyWorkspaceEditResponse -> Maybe String

  Hints:
  
FromJSON ApplyWorkspaceEditResponse
  
ToJSON ApplyWorkspaceEditResponse
.applied : ApplyWorkspaceEditResponse -> Bool
  Totality: total
  Visibility: public export
applied : ApplyWorkspaceEditResponse -> Bool
  Totality: total
  Visibility: public export
.failureReason : ApplyWorkspaceEditResponse -> Maybe String
  Totality: total
  Visibility: public export
failureReason : ApplyWorkspaceEditResponse -> Maybe String
  Totality: total
  Visibility: public export
.failedChange : ApplyWorkspaceEditResponse -> Maybe Integer
  Totality: total
  Visibility: public export
failedChange : ApplyWorkspaceEditResponse -> Maybe Integer
  Totality: total
  Visibility: public export
data FileOperationPatternKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructors:
  
FileKind : FileOperationPatternKind
  
FolderKind : FileOperationPatternKind

  Hints:
  
FromJSON FileOperationPatternKind
  
ToJSON FileOperationPatternKind
record FileOperationPatternOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileOperationPatternOptions : Maybe Bool -> FileOperationPatternOptions

  Projection: 
.ignoreCase : FileOperationPatternOptions -> Maybe Bool

  Hints:
  
FromJSON FileOperationPatternOptions
  
ToJSON FileOperationPatternOptions
.ignoreCase : FileOperationPatternOptions -> Maybe Bool
  Totality: total
  Visibility: public export
ignoreCase : FileOperationPatternOptions -> Maybe Bool
  Totality: total
  Visibility: public export
record FileOperationPattern : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileOperationPattern : String -> Maybe FileOperationPatternKind -> FileOperationPatternOptions -> FileOperationPattern

  Projections:
  
.glob : FileOperationPattern -> String
  
.matches : FileOperationPattern -> Maybe FileOperationPatternKind
  
.options : FileOperationPattern -> FileOperationPatternOptions

  Hints:
  
FromJSON FileOperationPattern
  
ToJSON FileOperationPattern
.glob : FileOperationPattern -> String
  Totality: total
  Visibility: public export
glob : FileOperationPattern -> String
  Totality: total
  Visibility: public export
.matches : FileOperationPattern -> Maybe FileOperationPatternKind
  Totality: total
  Visibility: public export
matches : FileOperationPattern -> Maybe FileOperationPatternKind
  Totality: total
  Visibility: public export
.options : FileOperationPattern -> FileOperationPatternOptions
  Totality: total
  Visibility: public export
options : FileOperationPattern -> FileOperationPatternOptions
  Totality: total
  Visibility: public export
record FileOperationFilter : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileOperationFilter : Maybe String -> FileOperationPattern -> FileOperationFilter

  Projections:
  
.pattern : FileOperationFilter -> FileOperationPattern
  
.scheme : FileOperationFilter -> Maybe String

  Hints:
  
FromJSON FileOperationFilter
  
ToJSON FileOperationFilter
.scheme : FileOperationFilter -> Maybe String
  Totality: total
  Visibility: public export
scheme : FileOperationFilter -> Maybe String
  Totality: total
  Visibility: public export
.pattern : FileOperationFilter -> FileOperationPattern
  Totality: total
  Visibility: public export
pattern : FileOperationFilter -> FileOperationPattern
  Totality: total
  Visibility: public export
record FileOperationRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileOperationRegistrationOptions : List FileOperationFilter -> FileOperationRegistrationOptions

  Projection: 
.filters : FileOperationRegistrationOptions -> List FileOperationFilter

  Hints:
  
FromJSON FileOperationRegistrationOptions
  
ToJSON FileOperationRegistrationOptions
.filters : FileOperationRegistrationOptions -> List FileOperationFilter
  Totality: total
  Visibility: public export
filters : FileOperationRegistrationOptions -> List FileOperationFilter
  Totality: total
  Visibility: public export
record FileCreate : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileCreate : URI -> FileCreate

  Projection: 
.uri : FileCreate -> URI

  Hints:
  
FromJSON FileCreate
  
ToJSON FileCreate
.uri : FileCreate -> URI
  Totality: total
  Visibility: public export
uri : FileCreate -> URI
  Totality: total
  Visibility: public export
record CreateFilesParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkCreateFilesParams : List FileCreate -> CreateFilesParams

  Projection: 
.files : CreateFilesParams -> List FileCreate

  Hints:
  
FromJSON CreateFilesParams
  
ToJSON CreateFilesParams
.files : CreateFilesParams -> List FileCreate
  Totality: total
  Visibility: public export
files : CreateFilesParams -> List FileCreate
  Totality: total
  Visibility: public export
record FileRename : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileRename : URI -> URI -> FileRename

  Projections:
  
.newUri : FileRename -> URI
  
.oldUri : FileRename -> URI

  Hints:
  
FromJSON FileRename
  
ToJSON FileRename
.oldUri : FileRename -> URI
  Totality: total
  Visibility: public export
oldUri : FileRename -> URI
  Totality: total
  Visibility: public export
.newUri : FileRename -> URI
  Totality: total
  Visibility: public export
newUri : FileRename -> URI
  Totality: total
  Visibility: public export
record RenameFilesParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkRenameFilesParams : List FileRename -> RenameFilesParams

  Projection: 
.files : RenameFilesParams -> List FileRename

  Hints:
  
FromJSON RenameFilesParams
  
ToJSON RenameFilesParams
.files : RenameFilesParams -> List FileRename
  Totality: total
  Visibility: public export
files : RenameFilesParams -> List FileRename
  Totality: total
  Visibility: public export
record FileDelete : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkFileDelete : URI -> FileDelete

  Projection: 
.uri : FileDelete -> URI

  Hints:
  
FromJSON FileDelete
  
ToJSON FileDelete
.uri : FileDelete -> URI
  Totality: total
  Visibility: public export
uri : FileDelete -> URI
  Totality: total
  Visibility: public export
record DeleteFilesParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles

  Totality: total
  Visibility: public export
  Constructor: 
MkDeleteFilesParams : List FileDelete -> DeleteFilesParams

  Projection: 
.files : DeleteFilesParams -> List FileDelete

  Hints:
  
FromJSON DeleteFilesParams
  
ToJSON DeleteFilesParams
.files : DeleteFilesParams -> List FileDelete
  Totality: total
  Visibility: public export
files : DeleteFilesParams -> List FileDelete
  Totality: total
  Visibility: public export