Idris2Doc : Language.LSP.Message.Progress

Language.LSP.Message.Progress

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

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

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressOptions : Maybe Bool -> WorkDoneProgressOptions

  Projection: 
.workDoneProgress : WorkDoneProgressOptions -> Maybe Bool

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

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressParams : Maybe ProgressToken -> WorkDoneProgressParams

  Projection: 
.workDoneToken : WorkDoneProgressParams -> Maybe ProgressToken

  Hints:
  
FromJSON WorkDoneProgressParams
  
ToJSON WorkDoneProgressParams
.workDoneToken : WorkDoneProgressParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
workDoneToken : WorkDoneProgressParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
record PartialResultParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#partialResultParams

  Totality: total
  Visibility: public export
  Constructor: 
MkPartialResultParams : Maybe ProgressToken -> PartialResultParams

  Projection: 
.partialResultToken : PartialResultParams -> Maybe ProgressToken

  Hints:
  
FromJSON PartialResultParams
  
ToJSON PartialResultParams
.partialResultToken : PartialResultParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
partialResultToken : PartialResultParams -> Maybe ProgressToken
  Totality: total
  Visibility: public export
record WorkDoneProgressBegin : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressBegin

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressBegin : String -> Maybe Bool -> Maybe String -> Maybe Int -> WorkDoneProgressBegin

  Projections:
  
.cancellable : WorkDoneProgressBegin -> Maybe Bool
  
.message : WorkDoneProgressBegin -> Maybe String
  
.percentage : WorkDoneProgressBegin -> Maybe Int
  
.title : WorkDoneProgressBegin -> String

  Hints:
  
FromJSON WorkDoneProgressBegin
  
ToJSON WorkDoneProgressBegin
.title : WorkDoneProgressBegin -> String
  Totality: total
  Visibility: public export
title : WorkDoneProgressBegin -> String
  Totality: total
  Visibility: public export
.cancellable : WorkDoneProgressBegin -> Maybe Bool
  Totality: total
  Visibility: public export
cancellable : WorkDoneProgressBegin -> Maybe Bool
  Totality: total
  Visibility: public export
.message : WorkDoneProgressBegin -> Maybe String
  Totality: total
  Visibility: public export
message : WorkDoneProgressBegin -> Maybe String
  Totality: total
  Visibility: public export
.percentage : WorkDoneProgressBegin -> Maybe Int
  Totality: total
  Visibility: public export
percentage : WorkDoneProgressBegin -> Maybe Int
  Totality: total
  Visibility: public export
record WorkDoneProgressReport : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressReport

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressReport : Maybe Bool -> Maybe String -> Maybe Int -> WorkDoneProgressReport

  Projections:
  
.cancellable : WorkDoneProgressReport -> Maybe Bool
  
.message : WorkDoneProgressReport -> Maybe String
  
.percentage : WorkDoneProgressReport -> Maybe Int

  Hints:
  
FromJSON WorkDoneProgressReport
  
ToJSON WorkDoneProgressReport
.cancellable : WorkDoneProgressReport -> Maybe Bool
  Totality: total
  Visibility: public export
cancellable : WorkDoneProgressReport -> Maybe Bool
  Totality: total
  Visibility: public export
.message : WorkDoneProgressReport -> Maybe String
  Totality: total
  Visibility: public export
message : WorkDoneProgressReport -> Maybe String
  Totality: total
  Visibility: public export
.percentage : WorkDoneProgressReport -> Maybe Int
  Totality: total
  Visibility: public export
percentage : WorkDoneProgressReport -> Maybe Int
  Totality: total
  Visibility: public export
record WorkDoneProgressEnd : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressEnd

  Totality: total
  Visibility: public export
  Constructor: 
MkWorkDoneProgressEnd : Maybe String -> WorkDoneProgressEnd

  Projection: 
.message : WorkDoneProgressEnd -> Maybe String

  Hints:
  
FromJSON WorkDoneProgressEnd
  
ToJSON WorkDoneProgressEnd
.message : WorkDoneProgressEnd -> Maybe String
  Totality: total
  Visibility: public export
message : WorkDoneProgressEnd -> Maybe String
  Totality: total
  Visibility: public export