Idris2Doc : Language.LSP.Message.Window

Language.LSP.Message.Window

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

  Totality: total
  Visibility: public export
  Constructors:
  
Error : MessageType
  
Warning : MessageType
  
Info : MessageType
  
Log : MessageType

  Hints:
  
FromJSON MessageType
  
ToJSON MessageType
record ShowMessageParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage

  Totality: total
  Visibility: public export
  Constructor: 
MkShowMessageParams : MessageType -> String -> ShowMessageParams

  Projections:
  
.message : ShowMessageParams -> String
  
.type : ShowMessageParams -> MessageType

  Hints:
  
FromJSON ShowMessageParams
  
ToJSON ShowMessageParams
.type : ShowMessageParams -> MessageType
  Totality: total
  Visibility: public export
type : ShowMessageParams -> MessageType
  Totality: total
  Visibility: public export
.message : ShowMessageParams -> String
  Totality: total
  Visibility: public export
message : ShowMessageParams -> String
  Totality: total
  Visibility: public export
record ShowMessageActionItem : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage

  Totality: total
  Visibility: public export
  Constructor: 
MkShowMessageActionItem : Maybe Bool -> ShowMessageActionItem

  Projection: 
.additionalPropertiesSupport : ShowMessageActionItem -> Maybe Bool

  Hints:
  
FromJSON ShowMessageActionItem
  
ToJSON ShowMessageActionItem
.additionalPropertiesSupport : ShowMessageActionItem -> Maybe Bool
  Totality: total
  Visibility: public export
additionalPropertiesSupport : ShowMessageActionItem -> Maybe Bool
  Totality: total
  Visibility: public export
record ShowMessageRequestClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage

  Totality: total
  Visibility: public export
  Constructor: 
MkShowMessageRequestClientCapabilities : Maybe ShowMessageActionItem -> ShowMessageRequestClientCapabilities

  Projection: 
.messageActionItem : ShowMessageRequestClientCapabilities -> Maybe ShowMessageActionItem

  Hints:
  
FromJSON ShowMessageRequestClientCapabilities
  
ToJSON ShowMessageRequestClientCapabilities
.messageActionItem : ShowMessageRequestClientCapabilities -> Maybe ShowMessageActionItem
  Totality: total
  Visibility: public export
messageActionItem : ShowMessageRequestClientCapabilities -> Maybe ShowMessageActionItem
  Totality: total
  Visibility: public export
record MessageActionItem : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage

  Totality: total
  Visibility: public export
  Constructor: 
MkMessageActionItem : String -> MessageActionItem

  Projection: 
.title : MessageActionItem -> String

  Hints:
  
FromJSON MessageActionItem
  
ToJSON MessageActionItem
.title : MessageActionItem -> String
  Totality: total
  Visibility: public export
title : MessageActionItem -> String
  Totality: total
  Visibility: public export
record ShowMessageRequestParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage

  Totality: total
  Visibility: public export
  Constructor: 
MkShowMessageRequestParams : MessageType -> String -> Maybe (List MessageActionItem) -> ShowMessageRequestParams

  Projections:
  
.actions : ShowMessageRequestParams -> Maybe (List MessageActionItem)
  
.message : ShowMessageRequestParams -> String
  
.type : ShowMessageRequestParams -> MessageType

  Hints:
  
FromJSON ShowMessageRequestParams
  
ToJSON ShowMessageRequestParams
.type : ShowMessageRequestParams -> MessageType
  Totality: total
  Visibility: public export
type : ShowMessageRequestParams -> MessageType
  Totality: total
  Visibility: public export
.message : ShowMessageRequestParams -> String
  Totality: total
  Visibility: public export
message : ShowMessageRequestParams -> String
  Totality: total
  Visibility: public export
.actions : ShowMessageRequestParams -> Maybe (List MessageActionItem)
  Totality: total
  Visibility: public export
actions : ShowMessageRequestParams -> Maybe (List MessageActionItem)
  Totality: total
  Visibility: public export
record ShowDocumentClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument

  Totality: total
  Visibility: public export
  Constructor: 
MkShowDocumentClientCapabilities : Bool -> ShowDocumentClientCapabilities

  Projection: 
.support : ShowDocumentClientCapabilities -> Bool

  Hints:
  
FromJSON ShowDocumentClientCapabilities
  
ToJSON ShowDocumentClientCapabilities
.support : ShowDocumentClientCapabilities -> Bool
  Totality: total
  Visibility: public export
support : ShowDocumentClientCapabilities -> Bool
  Totality: total
  Visibility: public export
record ShowDocumentParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument

  Totality: total
  Visibility: public export
  Constructor: 
MkShowDocumentParams : URI -> Maybe Bool -> Maybe Bool -> Maybe Range -> ShowDocumentParams

  Projections:
  
.external_ : ShowDocumentParams -> Maybe Bool
  
.selection : ShowDocumentParams -> Maybe Range
  
.takeFocus : ShowDocumentParams -> Maybe Bool
  
.uri : ShowDocumentParams -> URI

  Hints:
  
FromJSON ShowDocumentParams
  
ToJSON ShowDocumentParams
.uri : ShowDocumentParams -> URI
  Totality: total
  Visibility: public export
uri : ShowDocumentParams -> URI
  Totality: total
  Visibility: public export
.external_ : ShowDocumentParams -> Maybe Bool
  Totality: total
  Visibility: public export
external_ : ShowDocumentParams -> Maybe Bool
  Totality: total
  Visibility: public export
.takeFocus : ShowDocumentParams -> Maybe Bool
  Totality: total
  Visibility: public export
takeFocus : ShowDocumentParams -> Maybe Bool
  Totality: total
  Visibility: public export
.selection : ShowDocumentParams -> Maybe Range
  Totality: total
  Visibility: public export
selection : ShowDocumentParams -> Maybe Range
  Totality: total
  Visibility: public export
record ShowDocumentResult : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument

  Totality: total
  Visibility: public export
  Constructor: 
MkShowDocumentResult : Bool -> ShowDocumentResult

  Projection: 
.success : ShowDocumentResult -> Bool

  Hints:
  
FromJSON ShowDocumentResult
  
ToJSON ShowDocumentResult
.success : ShowDocumentResult -> Bool
  Totality: total
  Visibility: public export
success : ShowDocumentResult -> Bool
  Totality: total
  Visibility: public export
record LogMessageParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_logMessage

  Totality: total
  Visibility: public export
  Constructor: 
MkLogMessageParams : MessageType -> String -> LogMessageParams

  Projections:
  
.message : LogMessageParams -> String
  
.type : LogMessageParams -> MessageType

  Hints:
  
FromJSON LogMessageParams
  
ToJSON LogMessageParams
.type : LogMessageParams -> MessageType
  Totality: total
  Visibility: public export
type : LogMessageParams -> MessageType
  Totality: total
  Visibility: public export
.message : LogMessageParams -> String
  Totality: total
  Visibility: public export
message : LogMessageParams -> String
  Totality: total
  Visibility: public export
record WorkDoneProgressCreateParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_create

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressCreateParams : ProgressToken -> WorkDoneProgressCreateParams

  Projection: 
.token : WorkDoneProgressCreateParams -> ProgressToken

  Hints:
  
FromJSON WorkDoneProgressCreateParams
  
ToJSON WorkDoneProgressCreateParams
.token : WorkDoneProgressCreateParams -> ProgressToken
  Totality: total
  Visibility: public export
token : WorkDoneProgressCreateParams -> ProgressToken
  Totality: total
  Visibility: public export
record WorkDoneProgressCancelParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_cancel

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressCancelParams : ProgressToken -> WorkDoneProgressCancelParams

  Projection: 
.token : WorkDoneProgressCancelParams -> ProgressToken

  Hints:
  
FromJSON WorkDoneProgressCancelParams
  
ToJSON WorkDoneProgressCancelParams
.token : WorkDoneProgressCancelParams -> ProgressToken
  Totality: total
  Visibility: public export
token : WorkDoneProgressCancelParams -> ProgressToken
  Totality: total
  Visibility: public export