Language.LSP.Message.Location

Definitions

record Position : Type

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

Totality: total
Visibility: public export
Constructor: 

MkPosition : Int -> Int -> Position

Projections:

.character : Position -> Int

.line : Position -> Int

Hints:

Eq Position

FromJSON Position

ToJSON Position

.line : Position -> Int

Totality: total
Visibility: public export

line : Position -> Int

Totality: total
Visibility: public export

.character : Position -> Int

Totality: total
Visibility: public export

character : Position -> Int

Totality: total
Visibility: public export

record Range : Type

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

Totality: total
Visibility: public export
Constructor: 

MkRange : Position -> Position -> Range

Projections:

.end : Range -> Position

.start : Range -> Position

Hints:

Eq Range

FromJSON Range

ToJSON Range

.start : Range -> Position

Totality: total
Visibility: public export

start : Range -> Position

Totality: total
Visibility: public export

.end : Range -> Position

Totality: total
Visibility: public export

end : Range -> Position

Totality: total
Visibility: public export

record Location : Type

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

Totality: total
Visibility: public export
Constructor: 

MkLocation : URI -> Range -> Location

Projections:

.range : Location -> Range

.uri : Location -> URI

Hints:

Eq Location

FromJSON Location

ToJSON Location

.uri : Location -> URI

Totality: total
Visibility: public export

uri : Location -> URI

Totality: total
Visibility: public export

.range : Location -> Range

Totality: total
Visibility: public export

range : Location -> Range

Totality: total
Visibility: public export

record LocationLink : Type

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

Totality: total
Visibility: public export
Constructor: 

MkLocationLink : Maybe Range -> URI -> Range -> Range -> LocationLink

Projections:

.originSelectionRange : LocationLink -> Maybe Range

.targetRange : LocationLink -> Range

.targetSelectionRange : LocationLink -> Range

.targetUri : LocationLink -> URI

Hints:

FromJSON LocationLink

ToJSON LocationLink

.originSelectionRange : LocationLink -> Maybe Range

Totality: total
Visibility: public export

originSelectionRange : LocationLink -> Maybe Range

Totality: total
Visibility: public export

.targetUri : LocationLink -> URI

Totality: total
Visibility: public export

targetUri : LocationLink -> URI

Totality: total
Visibility: public export

.targetRange : LocationLink -> Range

Totality: total
Visibility: public export

targetRange : LocationLink -> Range

Totality: total
Visibility: public export

.targetSelectionRange : LocationLink -> Range

Totality: total
Visibility: public export

targetSelectionRange : LocationLink -> Range

Totality: total
Visibility: public export