Idris2Doc : Language.LSP.Message.Initialize

Language.LSP.Message.Initialize

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

  Totality: total
  Visibility: public export
  Constructor: 
__mkClientInfo : _

  Projections:
  
.name : ClientInfo -> String
  
.version : ClientInfo -> Maybe String

  Hints:
  
FromJSON ClientInfo
  
ToJSON ClientInfo
.name : ClientInfo -> String
  Totality: total
  Visibility: public export
name : ClientInfo -> String
  Totality: total
  Visibility: public export
.version : ClientInfo -> Maybe String
  Totality: total
  Visibility: public export
version : ClientInfo -> Maybe String
  Totality: total
  Visibility: public export
record InitializeParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize

  Totality: total
  Visibility: public export
  Constructor: 
MkInitializeParams : OneOf [Integer, Null] -> Maybe ClientInfo -> Maybe String -> Maybe (OneOf [String, Null]) -> OneOf [URI, Null] -> Maybe JSON -> ClientCapabilities -> Maybe Trace -> Maybe (OneOf [List WorkspaceFolder, Null]) -> Maybe ProgressToken -> InitializeParams

  Projections:
  
.capabilities : InitializeParams -> ClientCapabilities
  
.clientInfo : InitializeParams -> Maybe ClientInfo
  
.initializationOptions : InitializeParams -> Maybe JSON
  
.locale : InitializeParams -> Maybe String
  
.processId : InitializeParams -> OneOf [Integer, Null]
  
.rootPath : InitializeParams -> Maybe (OneOf [String, Null])
  
.rootUri : InitializeParams -> OneOf [URI, Null]
  
.trace : InitializeParams -> Maybe Trace
  
.workDoneToken : InitializeParams -> Maybe ProgressToken
  
.workspaceFolders : InitializeParams -> Maybe (OneOf [List WorkspaceFolder, Null])

  Hints:
  
FromJSON InitializeParams
  
ToJSON InitializeParams
.processId : InitializeParams -> OneOf [Integer, Null]
  Totality: total
  Visibility: public export
processId : InitializeParams -> OneOf [Integer, Null]
  Totality: total
  Visibility: public export
.clientInfo : InitializeParams -> Maybe ClientInfo
  Totality: total
  Visibility: public export
clientInfo : InitializeParams -> Maybe ClientInfo
  Totality: total
  Visibility: public export
.locale : InitializeParams -> Maybe String
  Totality: total
  Visibility: public export
locale : InitializeParams -> Maybe String
  Totality: total
  Visibility: public export
.rootPath : InitializeParams -> Maybe (OneOf [String, Null])
  Totality: total
  Visibility: public export
rootPath : InitializeParams -> Maybe (OneOf [String, Null])
  Totality: total
  Visibility: public export
.rootUri : InitializeParams -> OneOf [URI, Null]
  Totality: total
  Visibility: public export
rootUri : InitializeParams -> OneOf [URI, Null]
  Totality: total
  Visibility: public export
.initializationOptions : InitializeParams -> Maybe JSON
  Totality: total
  Visibility: public export
initializationOptions : InitializeParams -> Maybe JSON
  Totality: total
  Visibility: public export
.capabilities : InitializeParams -> ClientCapabilities
  Totality: total
  Visibility: public export
capabilities : InitializeParams -> ClientCapabilities
  Totality: total
  Visibility: public export
.trace : InitializeParams -> Maybe Trace
  Totality: total
  Visibility: public export
trace : InitializeParams -> Maybe Trace
  Totality: total
  Visibility: public export
.workspaceFolders : InitializeParams -> Maybe (OneOf [List WorkspaceFolder, Null])
  Totality: total
  Visibility: public export
workspaceFolders : InitializeParams -> Maybe (OneOf [List WorkspaceFolder, Null])
  Totality: total
  Visibility: public export
.workDoneToken : InitializeParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : InitializeParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
record InitializeResult : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize

  Totality: total
  Visibility: public export
  Constructor: 
MkInitializeResult : ServerCapabilities -> Maybe ServerInfo -> InitializeResult

  Projections:
  
.capabilities : InitializeResult -> ServerCapabilities
  
.serverInfo : InitializeResult -> Maybe ServerInfo

  Hints:
  
FromJSON InitializeResult
  
ToJSON InitializeResult
.capabilities : InitializeResult -> ServerCapabilities
  Totality: total
  Visibility: public export
capabilities : InitializeResult -> ServerCapabilities
  Totality: total
  Visibility: public export
.serverInfo : InitializeResult -> Maybe ServerInfo
  Totality: total
  Visibility: public export
serverInfo : InitializeResult -> Maybe ServerInfo
  Totality: total
  Visibility: public export
record InitializeError : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize

  Totality: total
  Visibility: public export
  Constructor: 
MkInitializeError : Bool -> InitializeError

  Projection: 
.retry : InitializeError -> Bool

  Hints:
  
FromJSON InitializeError
  
ToJSON InitializeError
.retry : InitializeError -> Bool
  Totality: total
  Visibility: public export
retry : InitializeError -> Bool
  Totality: total
  Visibility: public export
data InitializedParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialized

  Totality: total
  Visibility: public export
  Constructor: 
MkInitializedParams : InitializedParams

  Hints:
  
FromJSON InitializedParams
  
ToJSON InitializedParams