Language.LSP.Message.Markup

Definitions

data MarkupKind : Type

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

Totality: total
Visibility: public export
Constructors:

PlainText : MarkupKind

Markdown : MarkupKind

Hints:

Eq MarkupKind

FromJSON MarkupKind

ToJSON MarkupKind

record MarkupContent : Type

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

Totality: total
Visibility: public export
Constructor: 

MkMarkupContent : MarkupKind -> String -> MarkupContent

Projections:

.kind : MarkupContent -> MarkupKind

.value : MarkupContent -> String

Hints:

FromJSON MarkupContent

ToJSON MarkupContent

.kind : MarkupContent -> MarkupKind

Totality: total
Visibility: public export

kind : MarkupContent -> MarkupKind

Totality: total
Visibility: public export

.value : MarkupContent -> String

Totality: total
Visibility: public export

value : MarkupContent -> String

Totality: total
Visibility: public export

record MarkedStringWithLanguage : Type

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

Totality: total
Visibility: public export
Constructor: 

MkMarkedStringWithLanguage : String -> String -> MarkedStringWithLanguage

Projections:

.language : MarkedStringWithLanguage -> String

.value : MarkedStringWithLanguage -> String

Hints:

FromJSON MarkedStringWithLanguage

ToJSON MarkedStringWithLanguage

.language : MarkedStringWithLanguage -> String

Totality: total
Visibility: public export

language : MarkedStringWithLanguage -> String

Totality: total
Visibility: public export

.value : MarkedStringWithLanguage -> String

Totality: total
Visibility: public export

value : MarkedStringWithLanguage -> String

Totality: total
Visibility: public export

MarkedString : Type

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

Totality: total
Visibility: public export

record MarkdownClientCapabilities : Type

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

Totality: total
Visibility: public export
Constructor: 

MkMarkdownClientCapabilities : String -> Maybe String -> MarkdownClientCapabilities

Projections:

.parser : MarkdownClientCapabilities -> String

.version : MarkdownClientCapabilities -> Maybe String

Hints:

FromJSON MarkdownClientCapabilities

ToJSON MarkdownClientCapabilities

.parser : MarkdownClientCapabilities -> String

Totality: total
Visibility: public export

parser : MarkdownClientCapabilities -> String

Totality: total
Visibility: public export

.version : MarkdownClientCapabilities -> Maybe String

Totality: total
Visibility: public export

version : MarkdownClientCapabilities -> Maybe String

Totality: total
Visibility: public export