HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Highlighting.Precise

Types used for precise syntax highlighting.

  • 11 types
  • 2 classes
  • 9 values
  • PackageAgda-2.7.0.1
  • Exports22
  • LanguageHaskell2010
  • LicenceMIT
  • SourcePrecise.hs

Highlighting information

15 declarations
datadata Aspect
#

Constructors

Instances7Eq, Show, Generic, Semigroup, NFData, EmbPrj, …
datadata NameKind
#

NameKinds are figured out during scope checking.

Constructors

Instances7Eq, Show, Generic, Semigroup, NFData, EmbPrj, …
datadata OtherAspect
#

Other aspects, generated by type checking. (These can overlap with each other and with Aspects.)

Constructors

Instances9Bounded, Enum, Eq, Ord, Show, Generic, …
datadata Aspects
#

Syntactic aspects of the code. (These cannot overlap.)

Meta information which can be associated with a character/character range.

Constructors

Instances34Eq, Show, Generic, Monoid, NFData, ToJSON, …
datadata DefinitionSite
#

Constructors

Instances7Eq, Show, Generic, Semigroup, NFData, EmbPrj, …
datadata TokenBased
#

Is the highlighting "token-based", i.e. based only on information from the lexer?

TokenBasedNotOnlyTokenBased
Instances7Eq, Show, Semigroup, Monoid, ToJSON, EncodeTCM, …
  • Eq TokenBasedDefined in Agda-2.7.0.1 · Agda.Syntax.Common.Aspect
  • Show TokenBasedDefined in Agda-2.7.0.1 · Agda.Syntax.Common.Aspect
  • Semigroup TokenBasedDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Precise · orphan
  • Monoid TokenBasedDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Precise · orphan
  • ToJSON TokenBasedDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.JSON · orphan
  • EncodeTCM TokenBasedDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.JSON · orphan
  • EmbPrj TokenBasedDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Highlighting · orphan
newtypenewtype RangePair
#

A limited kind of syntax highlighting information: a pair consisting of Ranges and Aspects.

Note the invariant which RangePairs should satisfy (rangePairInvariant).

Constructors

Instances7Show, Monoid, NFData, IsBasicRangeMap, Convert, …
newtypenewtype PositionMap
#

Syntax highlighting information, represented by maps from positions to Aspects.

The first position in the file has number 1.

Constructors

Instances9Show, Semigroup, Monoid, NFData, IsBasicRangeMap, Convert, …
newtypenewtype DelayedMerge hl
#

Highlighting info with delayed merging.

Merging large sets of highlighting info repeatedly might be costly. The idea of this type is to accumulate small pieces of highlighting information, and then to merge them all at the end.

Note the invariant which values of this type should satisfy (delayedMergeInvariant).

Constructors

Instances11IsBasicRangeMap, Show, Semigroup, Monoid, Convert, …

Operations

classclass IsBasicRangeMap a m | m -> a where
#

A class that is intended to make it easy to swap between different range map implementations.

Note that some RangeMap operations are not included in this class.

Methods

  • singleton :: Ranges -> a -> m

    The map singleton rs x contains the ranges from rs, and every position in those ranges is associated with x.

  • toMap :: m -> IntMap a

    Converts range maps to IntMaps from positions to values.

  • toList :: m -> [(Range, a)]

    Converts the map to a list. The ranges are non-overlapping and non-empty, and earlier ranges precede later ones in the list.

  • coveringRange :: m -> Maybe Range

    Returns the smallest range covering everything in the map (or Nothing, if the range would be empty).

    Note that the default implementation of this operation might be inefficient.

Instances6IsBasicRangeMap
classclass Convert a b where
#

Conversion between different types.

Methods

Instances6Convert

Orphan instances

9 instances