Idris2Doc : Language.LSP.Message.DocumentSymbols

Language.LSP.Message.DocumentSymbols

(source)
Definitions
data SymbolKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructors:
  
File : SymbolKind
  
Module : SymbolKind
  
Namespace : SymbolKind
  
Package : SymbolKind
  
Class : SymbolKind
  
Method : SymbolKind
  
Property : SymbolKind
  
Field : SymbolKind
  
Constructor : SymbolKind
  
Enum : SymbolKind
  
Interface : SymbolKind
  
Function : SymbolKind
  
Variable : SymbolKind
  
Constant : SymbolKind
  
String_ : SymbolKind
  
Number : SymbolKind
  
Boolean : SymbolKind
  
Array : SymbolKind
  
Object : SymbolKind
  
Key : SymbolKind
  
Null : SymbolKind
  
EnumMember : SymbolKind
  
Struct : SymbolKind
  
Event : SymbolKind
  
Operator : SymbolKind
  
TypeParameter : SymbolKind

  Hints:
  
FromJSON SymbolKind
  
ToJSON SymbolKind
data SymbolTag : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
Deprecated : SymbolTag

  Hints:
  
FromJSON SymbolTag
  
ToJSON SymbolTag
record DocumentSymbolKind : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbolKind : Maybe (List SymbolKind) -> DocumentSymbolKind

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

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

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbolTag : Maybe (List SymbolTag) -> DocumentSymbolTag

  Projection: 
.valueSet : DocumentSymbolTag -> Maybe (List SymbolTag)

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

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbolClientCapabilities : Maybe Bool -> Maybe DocumentSymbolKind -> Maybe Bool -> Maybe DocumentSymbolTag -> Maybe Bool -> DocumentSymbolClientCapabilities

  Projections:
  
.dynamicRegistration : DocumentSymbolClientCapabilities -> Maybe Bool
  
.hierarchicalDocumentSymbolSupport : DocumentSymbolClientCapabilities -> Maybe Bool
  
.labelSupport : DocumentSymbolClientCapabilities -> Maybe Bool
  
.symbolKind : DocumentSymbolClientCapabilities -> Maybe DocumentSymbolKind
  
.tagSupport : DocumentSymbolClientCapabilities -> Maybe DocumentSymbolTag

  Hints:
  
FromJSON DocumentSymbolClientCapabilities
  
ToJSON DocumentSymbolClientCapabilities
.dynamicRegistration : DocumentSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dynamicRegistration : DocumentSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.symbolKind : DocumentSymbolClientCapabilities -> Maybe DocumentSymbolKind
  Totality: total
  Visibility: public export
symbolKind : DocumentSymbolClientCapabilities -> Maybe DocumentSymbolKind
  Totality: total
  Visibility: public export
.hierarchicalDocumentSymbolSupport : DocumentSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
hierarchicalDocumentSymbolSupport : DocumentSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.tagSupport : DocumentSymbolClientCapabilities -> Maybe DocumentSymbolTag
  Totality: total
  Visibility: public export
tagSupport : DocumentSymbolClientCapabilities -> Maybe DocumentSymbolTag
  Totality: total
  Visibility: public export
.labelSupport : DocumentSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
labelSupport : DocumentSymbolClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
record DocumentSymbolOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbolOptions : Maybe Bool -> Maybe String -> DocumentSymbolOptions

  Projections:
  
.label : DocumentSymbolOptions -> Maybe String
  
.workDoneProgress : DocumentSymbolOptions -> Maybe Bool

  Hints:
  
FromJSON DocumentSymbolOptions
  
ToJSON DocumentSymbolOptions
.workDoneProgress : DocumentSymbolOptions -> Maybe Bool
  Totality: total
  Visibility: public export
workDoneProgress : DocumentSymbolOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.label : DocumentSymbolOptions -> Maybe String
  Totality: total
  Visibility: public export
label : DocumentSymbolOptions -> Maybe String
  Totality: total
  Visibility: public export
record DocumentSymbolRegistrationOptions : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbolRegistrationOptions : Maybe Bool -> OneOf [DocumentSelector, Null] -> Maybe String -> DocumentSymbolRegistrationOptions

  Projections:
  
.documentSelector : DocumentSymbolRegistrationOptions -> OneOf [DocumentSelector, Null]
  
.label : DocumentSymbolRegistrationOptions -> Maybe String
  
.workDoneProgress : DocumentSymbolRegistrationOptions -> Maybe Bool

  Hints:
  
FromJSON DocumentSymbolRegistrationOptions
  
ToJSON DocumentSymbolRegistrationOptions
.workDoneProgress : DocumentSymbolRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
workDoneProgress : DocumentSymbolRegistrationOptions -> Maybe Bool
  Totality: total
  Visibility: public export
.documentSelector : DocumentSymbolRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
documentSelector : DocumentSymbolRegistrationOptions -> OneOf [DocumentSelector, Null]
  Totality: total
  Visibility: public export
.label : DocumentSymbolRegistrationOptions -> Maybe String
  Totality: total
  Visibility: public export
label : DocumentSymbolRegistrationOptions -> Maybe String
  Totality: total
  Visibility: public export
record DocumentSymbolParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbolParams : Maybe ProgressToken -> Maybe ProgressToken -> TextDocumentIdentifier -> DocumentSymbolParams

  Projections:
  
.partialResultToken : DocumentSymbolParams -> Maybe ProgressToken
  
.textDocument : DocumentSymbolParams -> TextDocumentIdentifier
  
.workDoneToken : DocumentSymbolParams -> Maybe ProgressToken

  Hints:
  
FromJSON DocumentSymbolParams
  
ToJSON DocumentSymbolParams
.workDoneToken : DocumentSymbolParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : DocumentSymbolParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.partialResultToken : DocumentSymbolParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : DocumentSymbolParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
.textDocument : DocumentSymbolParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
textDocument : DocumentSymbolParams -> TextDocumentIdentifier
  Totality: total
  Visibility: public export
record DocumentSymbol : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
MkDocumentSymbol : String -> Maybe String -> SymbolKind -> Maybe (List SymbolTag) -> Maybe Bool -> Range -> Range -> Maybe (List (Inf DocumentSymbol)) -> DocumentSymbol

  Projections:
  
.children : DocumentSymbol -> Maybe (List (Inf DocumentSymbol))
  
.deprecated : DocumentSymbol -> Maybe Bool
  
.detail : DocumentSymbol -> Maybe String
  
.kind : DocumentSymbol -> SymbolKind
  
.name : DocumentSymbol -> String
  
.range : DocumentSymbol -> Range
  
.selectionRange : DocumentSymbol -> Range
  
.tags : DocumentSymbol -> Maybe (List SymbolTag)

  Hints:
  
FromJSON DocumentSymbol
  
ToJSON DocumentSymbol
.name : DocumentSymbol -> String
  Totality: total
  Visibility: public export
name : DocumentSymbol -> String
  Totality: total
  Visibility: public export
.detail : DocumentSymbol -> Maybe String
  Totality: total
  Visibility: public export
detail : DocumentSymbol -> Maybe String
  Totality: total
  Visibility: public export
.kind : DocumentSymbol -> SymbolKind
  Totality: total
  Visibility: public export
kind : DocumentSymbol -> SymbolKind
  Totality: total
  Visibility: public export
.tags : DocumentSymbol -> Maybe (List SymbolTag)
  Totality: total
  Visibility: public export
tags : DocumentSymbol -> Maybe (List SymbolTag)
  Totality: total
  Visibility: public export
.deprecated : DocumentSymbol -> Maybe Bool
  Totality: total
  Visibility: public export
deprecated : DocumentSymbol -> Maybe Bool
  Totality: total
  Visibility: public export
.range : DocumentSymbol -> Range
  Totality: total
  Visibility: public export
range : DocumentSymbol -> Range
  Totality: total
  Visibility: public export
.selectionRange : DocumentSymbol -> Range
  Totality: total
  Visibility: public export
selectionRange : DocumentSymbol -> Range
  Totality: total
  Visibility: public export
.children : DocumentSymbol -> Maybe (List (Inf DocumentSymbol))
  Totality: total
  Visibility: public export
children : DocumentSymbol -> Maybe (List (Inf DocumentSymbol))
  Totality: total
  Visibility: public export
record SymbolInformation : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol

  Totality: total
  Visibility: public export
  Constructor: 
MkSymbolInformation : String -> SymbolKind -> Maybe (List SymbolTag) -> Maybe Bool -> Location -> Maybe String -> SymbolInformation

  Projections:
  
.containerName : SymbolInformation -> Maybe String
  
.deprecated : SymbolInformation -> Maybe Bool
  
.kind : SymbolInformation -> SymbolKind
  
.location : SymbolInformation -> Location
  
.name : SymbolInformation -> String
  
.tags : SymbolInformation -> Maybe (List SymbolTag)

  Hints:
  
FromJSON SymbolInformation
  
ToJSON SymbolInformation
.name : SymbolInformation -> String
  Totality: total
  Visibility: public export
name : SymbolInformation -> String
  Totality: total
  Visibility: public export
.kind : SymbolInformation -> SymbolKind
  Totality: total
  Visibility: public export
kind : SymbolInformation -> SymbolKind
  Totality: total
  Visibility: public export
.tags : SymbolInformation -> Maybe (List SymbolTag)
  Totality: total
  Visibility: public export
tags : SymbolInformation -> Maybe (List SymbolTag)
  Totality: total
  Visibility: public export
.deprecated : SymbolInformation -> Maybe Bool
  Totality: total
  Visibility: public export
deprecated : SymbolInformation -> Maybe Bool
  Totality: total
  Visibility: public export
.location : SymbolInformation -> Location
  Totality: total
  Visibility: public export
location : SymbolInformation -> Location
  Totality: total
  Visibility: public export
.containerName : SymbolInformation -> Maybe String
  Totality: total
  Visibility: public export
containerName : SymbolInformation -> Maybe String
  Totality: total
  Visibility: public export