Agda.Interaction.Highlighting.Precise

Files

data Aspect

data NameKind

data OtherAspect

data Aspects

data DefinitionSite

data File

type HighlightingInfo

Creation

singleton

several

Merging

merge

Inspection

smallestPos

toMap

Compressed files

data CompressedFile

compressedFileInvariant

compress

decompress

noHighlightingInRange

Creation

singletonC

severalC

splitAtC

selectC

Inspection

smallestPosC

Merge

mergeC