Protocol.IDE.Highlight

Definitions

record Highlight : Type

Totality: total
Visibility: public export
Constructor: 

MkHighlight : FileContext -> String -> Bool -> String -> Decoration -> String -> String -> String -> Highlight

Projections:

.decor : Highlight -> Decoration

.docOverview : Highlight -> String

.isImplicit : Highlight -> Bool

.key : Highlight -> String

.location : Highlight -> FileContext

.name : Highlight -> String

.ns : Highlight -> String

.typ : Highlight -> String

Hints:

FromSExpable Highlight

SExpable Highlight

.location : Highlight -> FileContext

Totality: total
Visibility: public export

location : Highlight -> FileContext

Totality: total
Visibility: public export

.name : Highlight -> String

Totality: total
Visibility: public export

name : Highlight -> String

Totality: total
Visibility: public export

.isImplicit : Highlight -> Bool

Totality: total
Visibility: public export

isImplicit : Highlight -> Bool

Totality: total
Visibility: public export

.key : Highlight -> String

Totality: total
Visibility: public export

key : Highlight -> String

Totality: total
Visibility: public export

.decor : Highlight -> Decoration

Totality: total
Visibility: public export

decor : Highlight -> Decoration

Totality: total
Visibility: public export

.docOverview : Highlight -> String

Totality: total
Visibility: public export

docOverview : Highlight -> String

Totality: total
Visibility: public export

.typ : Highlight -> String

Totality: total
Visibility: public export

typ : Highlight -> String

Totality: total
Visibility: public export

.ns : Highlight -> String

Totality: total
Visibility: public export

ns : Highlight -> String

Totality: total
Visibility: public export

record LwHighlight : Type

Totality: total
Visibility: public export
Constructor: 

MkLwHighlight : FileContext -> Decoration -> LwHighlight

Projections:

.decor : LwHighlight -> Decoration

.location : LwHighlight -> FileContext

Hints:

FromSExpable LwHighlight

SExpable LwHighlight

.location : LwHighlight -> FileContext

Totality: total
Visibility: public export

location : LwHighlight -> FileContext

Totality: total
Visibility: public export

.decor : LwHighlight -> Decoration

Totality: total
Visibility: public export

decor : LwHighlight -> Decoration

Totality: total
Visibility: public export

data SourceHighlight : Type

Totality: total
Visibility: public export
Constructors:

Full : Highlight -> SourceHighlight

Lw : LwHighlight -> SourceHighlight

Hints:

FromSExpable SourceHighlight

SExpable SourceHighlight