Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Interaction.Highlighting.Precise

Contents

Highlighting information
- Operations
Orphan instances

Description

Types used for precise syntax highlighting.

Synopsis

data Aspect
- = Comment
- | Keyword
- | String
- | Number
- | Hole
- | Symbol
- | PrimitiveType
- | Name (Maybe NameKind) Bool
- | Pragma
- | Background
- | Markup
data NameKind
- = Bound
- | Generalizable
- | Constructor Induction
- | Datatype
- | Field
- | Function
- | Module
- | Postulate
- | Primitive
- | Record
- | Argument
- | Macro
data OtherAspect
- = Error
- | ErrorWarning
- | DottedPattern
- | UnsolvedMeta
- | UnsolvedConstraint
- | TerminationProblem
- | PositivityProblem
- | Deadcode
- | ShadowingInTelescope
- | CoverageProblem
- | IncompletePattern
- | TypeChecks
- | MissingDefinition
- | CatchallClause
- | ConfluenceProblem
data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: String
- definitionSite :: Maybe DefinitionSite
- tokenBased :: !TokenBased
}
data DefinitionSite = DefinitionSite {
- defSiteModule :: TopLevelModuleName' Range
- defSitePos :: Int
- defSiteHere :: Bool
- defSiteAnchor :: Maybe String
}
data TokenBased
- = TokenBased
- | NotOnlyTokenBased
newtype RangePair = RangePair {
- rangePair :: (Ranges, Aspects)
}
rangePairInvariant :: RangePair -> Bool
newtype PositionMap = PositionMap {
- positionMap :: IntMap Aspects
}
newtype DelayedMerge hl = DelayedMerge (Endo [hl])
delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool
type HighlightingInfo = RangeMap Aspects
highlightingInfoInvariant :: HighlightingInfo -> Bool
type HighlightingInfoBuilder = DelayedMerge RangePair
highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool
parserBased :: Aspects
kindOfNameToNameKind :: KindOfName -> NameKind
class IsBasicRangeMap a m | m -> a where
- singleton :: Ranges -> a -> m
- toMap :: m -> IntMap a
- toList :: m -> [(Range, a)]
- coveringRange :: m -> Maybe Range
several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl
class Convert a b where
- convert :: a -> b
insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
restrictTo :: Range -> RangeMap a -> RangeMap a

Highlighting information

data Aspect Source #

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

Instances details

EmbPrj Aspect Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Int32 Source # icod_ :: Aspect -> S Int32 Source # value :: Int32 -> R Aspect Source #
Semigroup Aspect Source #	`NameKind` in `Name` can get more precise.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: Aspect -> Aspect -> Aspect # sconcat :: NonEmpty Aspect -> Aspect stimes :: Integral b => b -> Aspect -> Aspect
Generic Aspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect Associated Types type Rep Aspect :: Type -> Type Methods from :: Aspect -> Rep Aspect x to :: Rep Aspect x -> Aspect
Show Aspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Aspect -> ShowS show :: Aspect -> String showList :: [Aspect] -> ShowS
NFData Aspect
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: Aspect -> ()
Eq Aspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Aspect -> Aspect -> Bool (/=) :: Aspect -> Aspect -> Bool
type Rep Aspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4-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 Source #

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

Instances details

EmbPrj NameKind Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Int32 Source # icod_ :: NameKind -> S Int32 Source # value :: Int32 -> R NameKind Source #
Semigroup NameKind Source #	Some `NameKind`s are more informative than others.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: NameKind -> NameKind -> NameKind # sconcat :: NonEmpty NameKind -> NameKind stimes :: Integral b => b -> NameKind -> NameKind
Generic NameKind Source #
Instance details Defined in Agda.Syntax.Common.Aspect Associated Types type Rep NameKind :: Type -> Type Methods from :: NameKind -> Rep NameKind x to :: Rep NameKind x -> NameKind
Show NameKind Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> NameKind -> ShowS show :: NameKind -> String showList :: [NameKind] -> ShowS
NFData NameKind Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: NameKind -> ()
Eq NameKind Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: NameKind -> NameKind -> Bool (/=) :: NameKind -> NameKind -> Bool
type Rep NameKind Source #
Instance details Defined in Agda.Syntax.Common.Aspect type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.4-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 Source #

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

Instances details

EmbPrj OtherAspect Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Int32 Source # icod_ :: OtherAspect -> S Int32 Source # value :: Int32 -> R OtherAspect Source #
Bounded OtherAspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods minBound :: OtherAspect maxBound :: OtherAspect
Enum OtherAspect Source #
Instance details 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 Source #
Instance details Defined in Agda.Syntax.Common.Aspect Associated Types type Rep OtherAspect :: Type -> Type Methods from :: OtherAspect -> Rep OtherAspect x to :: Rep OtherAspect x -> OtherAspect
Show OtherAspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> OtherAspect -> ShowS show :: OtherAspect -> String showList :: [OtherAspect] -> ShowS
NFData OtherAspect
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: OtherAspect -> ()
Eq OtherAspect Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: OtherAspect -> OtherAspect -> Bool (/=) :: OtherAspect -> OtherAspect -> Bool
Ord OtherAspect Source #
Instance details 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 Source #
Instance details Defined in Agda.Syntax.Common.Aspect type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4-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 Source #

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

Instances details

EncodeTCM Doc Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Doc -> TCM Value Source #
Underscore Doc Source #
Instance details Defined in Agda.Syntax.Common Methods underscore :: Doc Source # isUnderscore :: Doc -> Bool Source #
ReportS Doc Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #
TraceS Doc Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #
EmbPrj Aspects Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspects -> S Int32 Source # icod_ :: Aspects -> S Int32 Source # value :: Int32 -> R Aspects Source #
EmbPrj Doc Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Int32 Source # icod_ :: Doc -> S Int32 Source # value :: Int32 -> R Doc Source #
Monoid Aspects
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: Aspects mappend :: Aspects -> Aspects -> Aspects mconcat :: [Aspects] -> Aspects
Semigroup Aspects Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: Aspects -> Aspects -> Aspects # sconcat :: NonEmpty Aspects -> Aspects stimes :: Integral b => b -> Aspects -> Aspects
Generic Aspects Source #
Instance details Defined in Agda.Syntax.Common.Aspect Associated Types type Rep Aspects :: Type -> Type Methods from :: Aspects -> Rep Aspects x to :: Rep Aspects x -> Aspects
Show Aspects Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Aspects -> ShowS show :: Aspects -> String showList :: [Aspects] -> ShowS
NFData Aspects
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: Aspects -> ()
Eq Aspects Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Aspects -> Aspects -> Bool (/=) :: Aspects -> Aspects -> Bool
ToJSON Doc Source #
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: Doc -> Value # toEncoding :: Doc -> Encoding # toJSONList :: [Doc] -> Value # toEncodingList :: [Doc] -> Encoding # omitField :: Doc -> Bool #
IsBasicRangeMap Aspects PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects RangePair Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
Convert PositionMap (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
ReportS (TCM Doc) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #
ReportS [Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #
ReportS [TCM Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #
TraceS (TCM Doc) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #
TraceS [Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #
TraceS [TCM Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #
Null (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods empty :: AbsToCon Doc Source # null :: AbsToCon Doc -> Bool Source #
Null (TCM Doc) Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc Source # null :: TCM Doc -> Bool Source #
IsString (AbsToCon Doc)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fromString :: String -> AbsToCon Doc
Semigroup (AbsToCon Doc) Source #
Instance details 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) Source #	This instance is more specific than a generic instance `Semigroup a => Semigroup (TCM a)`.
Instance details 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) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #
Convert (RangeMap Aspects) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: RangeMap Aspects -> RangeMap Aspects Source #
Monad m => Null (PureConversionT m Doc) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods empty :: PureConversionT m Doc Source # null :: PureConversionT m Doc -> Bool Source #
type Rep Aspects Source #
Instance details Defined in Agda.Syntax.Common.Aspect type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.4-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 Source #

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

Instances details

EmbPrj DefinitionSite Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Int32 Source # icod_ :: DefinitionSite -> S Int32 Source # value :: Int32 -> R DefinitionSite Source #
Semigroup DefinitionSite Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite # sconcat :: NonEmpty DefinitionSite -> DefinitionSite stimes :: Integral b => b -> DefinitionSite -> DefinitionSite
Generic DefinitionSite Source #
Instance details Defined in Agda.Syntax.Common.Aspect Associated Types type Rep DefinitionSite :: Type -> Type Methods from :: DefinitionSite -> Rep DefinitionSite x to :: Rep DefinitionSite x -> DefinitionSite
Show DefinitionSite Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> DefinitionSite -> ShowS show :: DefinitionSite -> String showList :: [DefinitionSite] -> ShowS
NFData DefinitionSite
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: DefinitionSite -> ()
Eq DefinitionSite Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: DefinitionSite -> DefinitionSite -> Bool (/=) :: DefinitionSite -> DefinitionSite -> Bool
type Rep DefinitionSite Source #
Instance details Defined in Agda.Syntax.Common.Aspect type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.4-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 Source #

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

Constructors

TokenBased
NotOnlyTokenBased

Instances

Instances details

EncodeTCM TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods encodeTCM :: TokenBased -> TCM Value Source #
EmbPrj TokenBased Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Int32 Source # icod_ :: TokenBased -> S Int32 Source # value :: Int32 -> R TokenBased Source #
Monoid TokenBased
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: TokenBased mappend :: TokenBased -> TokenBased -> TokenBased mconcat :: [TokenBased] -> TokenBased
Semigroup TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased # sconcat :: NonEmpty TokenBased -> TokenBased stimes :: Integral b => b -> TokenBased -> TokenBased
Show TokenBased Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> TokenBased -> ShowS show :: TokenBased -> String showList :: [TokenBased] -> ShowS
Eq TokenBased Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: TokenBased -> TokenBased -> Bool (/=) :: TokenBased -> TokenBased -> Bool
ToJSON TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods toJSON :: TokenBased -> Value # toEncoding :: TokenBased -> Encoding # toJSONList :: [TokenBased] -> Value # toEncodingList :: [TokenBased] -> Encoding # omitField :: TokenBased -> Bool #

newtype RangePair Source #

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

Instances details

Show RangePair Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> RangePair -> ShowS show :: RangePair -> String showList :: [RangePair] -> ShowS
NFData RangePair Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: RangePair -> ()
IsBasicRangeMap Aspects RangePair Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Convert (DelayedMerge RangePair) PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

rangePairInvariant :: RangePair -> Bool Source #

Invariant for RangePair.

newtype PositionMap Source #

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

Instances details

Monoid PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: PositionMap mappend :: PositionMap -> PositionMap -> PositionMap mconcat :: [PositionMap] -> PositionMap
Semigroup PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: PositionMap -> PositionMap -> PositionMap # sconcat :: NonEmpty PositionMap -> PositionMap stimes :: Integral b => b -> PositionMap -> PositionMap
Show PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> PositionMap -> ShowS show :: PositionMap -> String showList :: [PositionMap] -> ShowS
NFData PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: PositionMap -> ()
IsBasicRangeMap Aspects PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
Convert PositionMap (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
Convert (DelayedMerge RangePair) PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #

newtype DelayedMerge hl Source #

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

Instances details

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source # toMap :: DelayedMerge (RangeMap a) -> IntMap a Source # toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source # coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #
Monoid (DelayedMerge hl) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> DelayedMerge hl -> ShowS show :: DelayedMerge hl -> String showList :: [DelayedMerge hl] -> ShowS
Convert (DelayedMerge RangePair) PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Monoid hl => Convert (DelayedMerge hl) hl Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

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

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 Source #

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 Source #

The invariant for HighlightingInfo.

type HighlightingInfoBuilder = DelayedMerge RangePair Source #

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 Source #

The invariant for HighlightingInfoBuilder.

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

Operations

parserBased :: Aspects Source #

A variant of mempty with tokenBased set to NotOnlyTokenBased.

kindOfNameToNameKind :: KindOfName -> NameKind Source #

Conversion from classification of the scope checker.

class IsBasicRangeMap a m | m -> a where Source #

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 Source #

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

toMap :: m -> IntMap a Source #

Converts range maps to IntMaps from positions to values.

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

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 Source #

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

Instances details

IsBasicRangeMap Aspects PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects RangePair Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source # toMap :: DelayedMerge (RangeMap a) -> IntMap a Source # toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source # coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #
IsBasicRangeMap a (RangeMap a) Source #
Instance details Defined in Agda.Utils.RangeMap Methods singleton :: Ranges -> a -> RangeMap a Source # toMap :: RangeMap a -> IntMap a Source # toList :: RangeMap a -> [(Range, a)] Source # coveringRange :: RangeMap a -> Maybe Range Source #

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

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

class Convert a b where Source #

Conversion between different types.

Methods

convert :: a -> b Source #

Instances

Instances details

Convert PositionMap (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Monoid hl => Convert (DelayedMerge hl) hl Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #
Convert (RangeMap Aspects) (RangeMap Aspects) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: RangeMap Aspects -> RangeMap Aspects Source #

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

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

restrictTo :: Range -> RangeMap a -> RangeMap a Source #

Restricts the RangeMap to the given range.

Orphan instances

Monoid Aspects Source #
Instance details Methods mempty :: Aspects mappend :: Aspects -> Aspects -> Aspects mconcat :: [Aspects] -> Aspects
Monoid TokenBased Source #
Instance details Methods mempty :: TokenBased mappend :: TokenBased -> TokenBased -> TokenBased mconcat :: [TokenBased] -> TokenBased
Semigroup Aspects Source #
Instance details Methods (<>) :: Aspects -> Aspects -> Aspects # sconcat :: NonEmpty Aspects -> Aspects stimes :: Integral b => b -> Aspects -> Aspects
Semigroup DefinitionSite Source #
Instance details Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite # sconcat :: NonEmpty DefinitionSite -> DefinitionSite stimes :: Integral b => b -> DefinitionSite -> DefinitionSite
Semigroup TokenBased Source #
Instance details Methods (<>) :: TokenBased -> TokenBased -> TokenBased # sconcat :: NonEmpty TokenBased -> TokenBased stimes :: Integral b => b -> TokenBased -> TokenBased
NFData Aspect Source #
Instance details Methods rnf :: Aspect -> ()
NFData Aspects Source #
Instance details Methods rnf :: Aspects -> ()
NFData DefinitionSite Source #
Instance details Methods rnf :: DefinitionSite -> ()
NFData OtherAspect Source #
Instance details Methods rnf :: OtherAspect -> ()