Agda.Interaction.Highlighting.Precise

Types used for precise syntax highlighting.

Highlighting information

data Aspect

Constructors

Comment

Keyword

String

Number

Hole

Symbol

Symbols like forall, =, ->, etc.

PrimitiveType

Things like Set and Prop.

Name (Maybe NameKind) Bool

Is the name an operator part?

Pragma

Text occurring in pragmas that does not have a more specific aspect.

Background

Non-code contents in literate Agda

Markup

Delimiters used to separate the Agda code blocks from the other contents in literate Agda

Instances

EmbPrj Aspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32

icod_ :: Aspect -> S Int32

value :: Int32 -> R Aspect

Semigroup Aspect

NameKind in Name can get more precise.

Defined in Agda.Syntax.Common.Aspect

Methods

(<>) :: Aspect -> Aspect -> Aspect

sconcat :: NonEmpty Aspect -> Aspect

stimes :: Integral b => b -> Aspect -> Aspect

Generic Aspect

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspect

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: Aspect -> Rep Aspect x

to :: Rep Aspect x -> Aspect

Show Aspect

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspect -> ShowS

show :: Aspect -> String

showList :: [Aspect] -> ShowS

NFData Aspect

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> ()

Eq Aspect

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Aspect -> Aspect -> Bool

(/=) :: Aspect -> Aspect -> Bool

type Rep Aspect

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

data NameKind

NameKinds are figured out during scope checking.

Constructors

Bound

Bound variable.

Generalizable

Generalizable variable. (This includes generalizable variables that have been generalized).

Constructor Induction

Inductive or coinductive constructor.

Datatype

Field

Record field.

Function

Module

Module name.

Postulate

Primitive

Primitive.

Record

Record type.

Argument

Named argument, like x in {x = v}

Macro

Macro.

Instances

EmbPrj NameKind

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32

icod_ :: NameKind -> S Int32

value :: Int32 -> R NameKind

Semigroup NameKind

Some NameKinds are more informative than others.

Defined in Agda.Syntax.Common.Aspect

Methods

(<>) :: NameKind -> NameKind -> NameKind

sconcat :: NonEmpty NameKind -> NameKind

stimes :: Integral b => b -> NameKind -> NameKind

Generic NameKind

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep NameKind

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: NameKind -> Rep NameKind x

to :: Rep NameKind x -> NameKind

Show NameKind

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> NameKind -> ShowS

show :: NameKind -> String

showList :: [NameKind] -> ShowS

NFData NameKind

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: NameKind -> ()

Eq NameKind

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: NameKind -> NameKind -> Bool

(/=) :: NameKind -> NameKind -> Bool

type Rep NameKind

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

data OtherAspect

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

Constructors

Error

ErrorWarning

A warning that is considered fatal in the end.

DottedPattern

UnsolvedMeta

UnsolvedConstraint

Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.

TerminationProblem

PositivityProblem

Deadcode

Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc.

ShadowingInTelescope

Used for shadowed repeated variable names in telescopes.

CoverageProblem

IncompletePattern

When this constructor is used it is probably a good idea to include a note explaining why the pattern is incomplete.

TypeChecks

Code which is being type-checked.

MissingDefinition

Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode.

CatchallClause

ConfluenceProblem

Instances

EmbPrj OtherAspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32

icod_ :: OtherAspect -> S Int32

value :: Int32 -> R OtherAspect

Bounded OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

minBound :: OtherAspect

maxBound :: OtherAspect

Enum OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

succ :: OtherAspect -> OtherAspect

pred :: OtherAspect -> OtherAspect

toEnum :: Int -> OtherAspect

fromEnum :: OtherAspect -> Int

enumFrom :: OtherAspect -> [OtherAspect]

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]

Generic OtherAspect

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep OtherAspect

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: OtherAspect -> Rep OtherAspect x

to :: Rep OtherAspect x -> OtherAspect

Show OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> OtherAspect -> ShowS

show :: OtherAspect -> String

showList :: [OtherAspect] -> ShowS

NFData OtherAspect

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: OtherAspect -> ()

Eq OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: OtherAspect -> OtherAspect -> Bool

(/=) :: OtherAspect -> OtherAspect -> Bool

Ord OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: OtherAspect -> OtherAspect -> Ordering

(<) :: OtherAspect -> OtherAspect -> Bool

(<=) :: OtherAspect -> OtherAspect -> Bool

(>) :: OtherAspect -> OtherAspect -> Bool

(>=) :: OtherAspect -> OtherAspect -> Bool

max :: OtherAspect -> OtherAspect -> OtherAspect

min :: OtherAspect -> OtherAspect -> OtherAspect

type Rep OtherAspect

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Aspects

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

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

Constructors

Aspects

Fields

• aspect :: Maybe Aspect
• otherAspects :: Set OtherAspect
• note :: String

  This note, if not null, can be displayed as a tool-tip or something like that. It should contain useful information about the range (like the module containing a certain identifier, or the fixity of an operator).

• definitionSite :: Maybe DefinitionSite

  The definition site of the annotated thing, if applicable and known.

• tokenBased :: !TokenBased

  Is this entry token-based?

Instances

EncodeTCM Doc

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value

Underscore Doc

Defined in Agda.Syntax.Common

Methods

underscore :: Doc

isUnderscore :: Doc -> Bool

ReportS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m ()

TraceS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c

EmbPrj Aspects

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32

icod_ :: Aspects -> S Int32

value :: Int32 -> R Aspects

EmbPrj Doc

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32

icod_ :: Doc -> S Int32

value :: Int32 -> R Doc

Monoid Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: Aspects

mappend :: Aspects -> Aspects -> Aspects

mconcat :: [Aspects] -> Aspects

Semigroup Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: Aspects -> Aspects -> Aspects

sconcat :: NonEmpty Aspects -> Aspects

stimes :: Integral b => b -> Aspects -> Aspects

Generic Aspects

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspects

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

Methods

from :: Aspects -> Rep Aspects x

to :: Rep Aspects x -> Aspects

Show Aspects

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspects -> ShowS

show :: Aspects -> String

showList :: [Aspects] -> ShowS

NFData Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspects -> ()

Eq Aspects

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Aspects -> Aspects -> Bool

(/=) :: Aspects -> Aspects -> Bool

ToJSON Doc

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value

toEncoding :: Doc -> Encoding

toJSONList :: [Doc] -> Value

toEncodingList :: [Doc] -> Encoding

omitField :: Doc -> Bool

IsBasicRangeMap Aspects PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap

toMap :: PositionMap -> IntMap Aspects

toList :: PositionMap -> [(Range, Aspects)]

coveringRange :: PositionMap -> Maybe Range

IsBasicRangeMap Aspects RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair

toMap :: RangePair -> IntMap Aspects

toList :: RangePair -> [(Range, Aspects)]

coveringRange :: RangePair -> Maybe Range

Convert PositionMap (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects

IsBasicRangeMap Aspects (DelayedMerge PositionMap)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap

toMap :: DelayedMerge PositionMap -> IntMap Aspects

toList :: DelayedMerge PositionMap -> [(Range, Aspects)]

coveringRange :: DelayedMerge PositionMap -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge RangePair)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair

toMap :: DelayedMerge RangePair -> IntMap Aspects

toList :: DelayedMerge RangePair -> [(Range, Aspects)]

coveringRange :: DelayedMerge RangePair -> Maybe Range

ReportS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()

ReportS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m ()

ReportS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m ()

TraceS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c

TraceS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c

TraceS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c

Null (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

empty :: AbsToCon Doc

null :: AbsToCon Doc -> Bool

Null (TCM Doc)

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc

null :: TCM Doc -> Bool

IsString (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fromString :: String -> AbsToCon Doc

Semigroup (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc

sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc

stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc

Semigroup (TCM Doc)

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

Defined in Agda.TypeChecking.Pretty

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

Convert (DelayedMerge PositionMap) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects

Convert (DelayedMerge RangePair) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects

Convert (RangeMap Aspects) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: RangeMap Aspects -> RangeMap Aspects

Monad m => Null (PureConversionT m Doc)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc

null :: PureConversionT m Doc -> Bool

type Rep Aspects

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

data DefinitionSite

Constructors

DefinitionSite

Fields

• defSiteModule :: TopLevelModuleName' Range

  The defining module.

• defSitePos :: Int

  The file position in that module. File positions are counted from 1.

• defSiteHere :: Bool

  Has this DefinitionSite been created at the defining site of the name?

• defSiteAnchor :: Maybe String

  A pretty name for the HTML linking.

Instances

EmbPrj DefinitionSite

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32

icod_ :: DefinitionSite -> S Int32

value :: Int32 -> R DefinitionSite

Semigroup DefinitionSite

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite

sconcat :: NonEmpty DefinitionSite -> DefinitionSite

stimes :: Integral b => b -> DefinitionSite -> DefinitionSite

Generic DefinitionSite

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep DefinitionSite

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

Methods

from :: DefinitionSite -> Rep DefinitionSite x

to :: Rep DefinitionSite x -> DefinitionSite

Show DefinitionSite

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> DefinitionSite -> ShowS

show :: DefinitionSite -> String

showList :: [DefinitionSite] -> ShowS

NFData DefinitionSite

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: DefinitionSite -> ()

Eq DefinitionSite

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: DefinitionSite -> DefinitionSite -> Bool

(/=) :: DefinitionSite -> DefinitionSite -> Bool

type Rep DefinitionSite

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

data TokenBased

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

Constructors

TokenBased

NotOnlyTokenBased

Instances

EncodeTCM TokenBased

Defined in Agda.Interaction.Highlighting.JSON

Methods

encodeTCM :: TokenBased -> TCM Value

EmbPrj TokenBased

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32

icod_ :: TokenBased -> S Int32

value :: Int32 -> R TokenBased

Monoid TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: TokenBased

mappend :: TokenBased -> TokenBased -> TokenBased

mconcat :: [TokenBased] -> TokenBased

Semigroup TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: TokenBased -> TokenBased -> TokenBased

sconcat :: NonEmpty TokenBased -> TokenBased

stimes :: Integral b => b -> TokenBased -> TokenBased

Show TokenBased

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> TokenBased -> ShowS

show :: TokenBased -> String

showList :: [TokenBased] -> ShowS

Eq TokenBased

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: TokenBased -> TokenBased -> Bool

(/=) :: TokenBased -> TokenBased -> Bool

ToJSON TokenBased

Defined in Agda.Interaction.Highlighting.JSON

Methods

toJSON :: TokenBased -> Value

toEncoding :: TokenBased -> Encoding

toJSONList :: [TokenBased] -> Value

toEncodingList :: [TokenBased] -> Encoding

omitField :: TokenBased -> Bool

newtype RangePair

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

Note the invariant which RangePairs should satisfy (rangePairInvariant).

Constructors

RangePair

Fields

• rangePair :: (Ranges, Aspects)

Instances

Show RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> RangePair -> ShowS

show :: RangePair -> String

showList :: [RangePair] -> ShowS

NFData RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: RangePair -> ()

IsBasicRangeMap Aspects RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair

toMap :: RangePair -> IntMap Aspects

toList :: RangePair -> [(Range, Aspects)]

coveringRange :: RangePair -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge RangePair)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair

toMap :: DelayedMerge RangePair -> IntMap Aspects

toList :: DelayedMerge RangePair -> [(Range, Aspects)]

coveringRange :: DelayedMerge RangePair -> Maybe Range

Convert (DelayedMerge RangePair) PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap

Convert (DelayedMerge RangePair) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects

rangePairInvariant :: RangePair -> Bool

Invariant for RangePair.

newtype PositionMap

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

The first position in the file has number 1.

Constructors

PositionMap

Fields

• positionMap :: IntMap Aspects

Instances

Monoid PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: PositionMap

mappend :: PositionMap -> PositionMap -> PositionMap

mconcat :: [PositionMap] -> PositionMap

Semigroup PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: PositionMap -> PositionMap -> PositionMap

sconcat :: NonEmpty PositionMap -> PositionMap

stimes :: Integral b => b -> PositionMap -> PositionMap

Show PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> PositionMap -> ShowS

show :: PositionMap -> String

showList :: [PositionMap] -> ShowS

NFData PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: PositionMap -> ()

IsBasicRangeMap Aspects PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap

toMap :: PositionMap -> IntMap Aspects

toList :: PositionMap -> [(Range, Aspects)]

coveringRange :: PositionMap -> Maybe Range

Convert PositionMap (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects

IsBasicRangeMap Aspects (DelayedMerge PositionMap)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap

toMap :: DelayedMerge PositionMap -> IntMap Aspects

toList :: DelayedMerge PositionMap -> [(Range, Aspects)]

coveringRange :: DelayedMerge PositionMap -> Maybe Range

Convert (DelayedMerge RangePair) PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap

Convert (DelayedMerge PositionMap) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects

newtype 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

DelayedMerge (Endo [hl])

Instances

IsBasicRangeMap Aspects (DelayedMerge PositionMap)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap

toMap :: DelayedMerge PositionMap -> IntMap Aspects

toList :: DelayedMerge PositionMap -> [(Range, Aspects)]

coveringRange :: DelayedMerge PositionMap -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge RangePair)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair

toMap :: DelayedMerge RangePair -> IntMap Aspects

toList :: DelayedMerge RangePair -> [(Range, Aspects)]

coveringRange :: DelayedMerge RangePair -> Maybe Range

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a))

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> a -> DelayedMerge (RangeMap a)

toMap :: DelayedMerge (RangeMap a) -> IntMap a

toList :: DelayedMerge (RangeMap a) -> [(Range, a)]

coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range

Monoid (DelayedMerge hl)

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: DelayedMerge hl

mappend :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl

mconcat :: [DelayedMerge hl] -> DelayedMerge hl

Semigroup (DelayedMerge hl)

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl

sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl

stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl

Show hl => Show (DelayedMerge hl)

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> DelayedMerge hl -> ShowS

show :: DelayedMerge hl -> String

showList :: [DelayedMerge hl] -> ShowS

Convert (DelayedMerge RangePair) PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap

Monoid hl => Convert (DelayedMerge hl) hl

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge hl -> hl

Convert (DelayedMerge PositionMap) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects

Convert (DelayedMerge RangePair) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects

delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool

Invariant for DelayedMerge hl, parametrised by the invariant for hl.

Additionally the endofunction should be extensionally equal to (fs ++) for some list fs.

type HighlightingInfo = RangeMap Aspects

Highlighting information.

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

This is a type synonym in order to make it easy to change to another representation.

highlightingInfoInvariant :: HighlightingInfo -> Bool

The invariant for HighlightingInfo.

type HighlightingInfoBuilder = DelayedMerge RangePair

A type that is intended to be used when constructing highlighting information.

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

This is a type synonym in order to make it easy to change to another representation.

The type should be an instance of IsBasicRangeMap Aspects, Semigroup and Monoid, and there should be an instance of Convert HighlightingInfoBuilder HighlightingInfo.

highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool

The invariant for HighlightingInfoBuilder.

Additionally the endofunction should be extensionally equal to (fs ++) for some list fs.

Operations

parserBased :: Aspects

A variant of mempty with tokenBased set to NotOnlyTokenBased.

kindOfNameToNameKind :: KindOfName -> NameKind

Conversion from classification of the scope checker.

class 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.

Minimal complete definition

singleton, toMap, toList

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.

Instances

IsBasicRangeMap Aspects PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap

toMap :: PositionMap -> IntMap Aspects

toList :: PositionMap -> [(Range, Aspects)]

coveringRange :: PositionMap -> Maybe Range

IsBasicRangeMap Aspects RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair

toMap :: RangePair -> IntMap Aspects

toList :: RangePair -> [(Range, Aspects)]

coveringRange :: RangePair -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge PositionMap)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap

toMap :: DelayedMerge PositionMap -> IntMap Aspects

toList :: DelayedMerge PositionMap -> [(Range, Aspects)]

coveringRange :: DelayedMerge PositionMap -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge RangePair)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair

toMap :: DelayedMerge RangePair -> IntMap Aspects

toList :: DelayedMerge RangePair -> [(Range, Aspects)]

coveringRange :: DelayedMerge RangePair -> Maybe Range

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a))

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> a -> DelayedMerge (RangeMap a)

toMap :: DelayedMerge (RangeMap a) -> IntMap a

toList :: DelayedMerge (RangeMap a) -> [(Range, a)]

coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range

IsBasicRangeMap a (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

singleton :: Ranges -> a -> RangeMap a

toMap :: RangeMap a -> IntMap a

toList :: RangeMap a -> [(Range, a)]

coveringRange :: RangeMap a -> Maybe Range

several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl

Like singleton, but with several Ranges instead of only one.

class Convert a b where

Conversion between different types.

Methods

convert :: a -> b

Instances

Convert PositionMap (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects

Convert (DelayedMerge RangePair) PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap

Monoid hl => Convert (DelayedMerge hl) hl

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge hl -> hl

Convert (DelayedMerge PositionMap) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects

Convert (DelayedMerge RangePair) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects

Convert (RangeMap Aspects) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: RangeMap Aspects -> RangeMap Aspects

insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)

Returns a RangeMap overlapping the given range, as well as the rest of the map.

restrictTo :: Range -> RangeMap a -> RangeMap a

Restricts the RangeMap to the given range.

Orphan instances

Monoid Aspects

Methods

mempty :: Aspects

mappend :: Aspects -> Aspects -> Aspects

mconcat :: [Aspects] -> Aspects

Monoid TokenBased

Methods

mempty :: TokenBased

mappend :: TokenBased -> TokenBased -> TokenBased

mconcat :: [TokenBased] -> TokenBased

Semigroup Aspects

Methods

(<>) :: Aspects -> Aspects -> Aspects

sconcat :: NonEmpty Aspects -> Aspects

stimes :: Integral b => b -> Aspects -> Aspects

Semigroup DefinitionSite

Methods

(<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite

sconcat :: NonEmpty DefinitionSite -> DefinitionSite

stimes :: Integral b => b -> DefinitionSite -> DefinitionSite

Semigroup TokenBased

Methods

(<>) :: TokenBased -> TokenBased -> TokenBased

sconcat :: NonEmpty TokenBased -> TokenBased

stimes :: Integral b => b -> TokenBased -> TokenBased

NFData Aspect

Methods

rnf :: Aspect -> ()

NFData Aspects

Methods

rnf :: Aspects -> ()

NFData DefinitionSite

Methods

rnf :: DefinitionSite -> ()

NFData OtherAspect

Methods

rnf :: OtherAspect -> ()