Language.LSP.Message.Trace

Definitions

data Trace : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#traceValue

Totality: total
Visibility: public export
Constructors:

TraceOff : Trace

TraceMessages : Trace

TraceVerbose : Trace

Hints:

FromJSON Trace

ToJSON Trace

record SetTraceParams : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#setTrace

Totality: total
Visibility: public export
Constructor: 

MkSetTraceParams : Trace -> SetTraceParams

Projection: 

.value : SetTraceParams -> Trace

Hints:

FromJSON SetTraceParams

ToJSON SetTraceParams

.value : SetTraceParams -> Trace

Totality: total
Visibility: public export

value : SetTraceParams -> Trace

Totality: total
Visibility: public export

record LogTraceParams : Type

  Refer to https://microsoft.github.io/language-server-protocol/specification.html#logTrace

Totality: total
Visibility: public export
Constructor: 

MkLogTraceParams : String -> Maybe String -> LogTraceParams

Projections:

.message : LogTraceParams -> String

.verbose : LogTraceParams -> Maybe String

Hints:

FromJSON LogTraceParams

ToJSON LogTraceParams

.message : LogTraceParams -> String

Totality: total
Visibility: public export

message : LogTraceParams -> String

Totality: total
Visibility: public export

.verbose : LogTraceParams -> Maybe String

Totality: total
Visibility: public export

verbose : LogTraceParams -> Maybe String

Totality: total
Visibility: public export