| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Highlighting.Precise
Description
Types used for precise syntax highlighting.
Synopsis
- data Aspect
- data NameKind
- data OtherAspect
- data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: String
- definitionSite :: Maybe DefinitionSite
- tokenBased :: !TokenBased
- data DefinitionSite = DefinitionSite {
- defSiteModule :: TopLevelModuleName
- defSitePos :: Int
- defSiteHere :: Bool
- defSiteAnchor :: Maybe String
- data TokenBased
- newtype RangePair = RangePair {}
- 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
- 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
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 Source # | |
| Semigroup Aspect Source # |
|
| Generic Aspect Source # | |
| Show Aspect Source # | |
| NFData Aspect | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Eq Aspect Source # | |
| type Rep Aspect Source # | |
Defined in Agda.Syntax.Common.Aspect type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-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))))) | |
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 Source # | |
| Semigroup NameKind Source # | Some |
| Generic NameKind Source # | |
| Show NameKind Source # | |
| NFData NameKind Source # | |
Defined in Agda.Syntax.Common.Aspect | |
| Eq NameKind Source # | |
| type Rep NameKind Source # | |
Defined in Agda.Syntax.Common.Aspect type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-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 |
| 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 Source # | |
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 # | |
Defined in Agda.Syntax.Common.Aspect | |
| Enum OtherAspect Source # | |
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 # | |
Defined in Agda.Syntax.Common.Aspect Associated Types type Rep OtherAspect :: Type -> Type | |
| Show OtherAspect Source # | |
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 Source # | |
Defined in Agda.Syntax.Common.Aspect | |
| Ord OtherAspect Source # | |
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 # | |
Defined in Agda.Syntax.Common.Aspect type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-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))))) | |
Syntactic aspects of the code. (These cannot overlap.)
Meta information which can be associated with a character/character range.
Constructors
| Aspects | |
Fields
| |
Instances
data DefinitionSite Source #
Constructors
| DefinitionSite | |
Fields
| |
Instances
| EmbPrj DefinitionSite Source # | |
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 # | |
Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite # sconcat :: NonEmpty DefinitionSite -> DefinitionSite stimes :: Integral b => b -> DefinitionSite -> DefinitionSite | |
| Generic DefinitionSite Source # | |
Defined in Agda.Syntax.Common.Aspect Associated Types type Rep DefinitionSite :: Type -> Type | |
| Show DefinitionSite Source # | |
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 Source # | |
Defined in Agda.Syntax.Common.Aspect Methods (==) :: DefinitionSite -> DefinitionSite -> Bool (/=) :: DefinitionSite -> DefinitionSite -> Bool | |
| type Rep DefinitionSite Source # | |
Defined in Agda.Syntax.Common.Aspect type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: 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
A limited kind of syntax highlighting information: a pair
consisting of Ranges and Aspects.
Note the invariant which RangePairs should satisfy
(rangePairInvariant).
Instances
| Show RangePair Source # | |
| NFData RangePair Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| IsBasicRangeMap Aspects RangePair Source # | |
| IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Convert (DelayedMerge RangePair) PositionMap Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods | |
| Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
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
| |
Instances
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
delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool Source #
Invariant for DelayedMerge hlhl.
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 AspectsSemigroup 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.
Methods
singleton :: Ranges -> a -> m Source #
The map singleton rs xrs, 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
several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl Source #
class Convert a b where Source #
Conversion between different types.
Instances
| Convert PositionMap (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Convert (DelayedMerge RangePair) PositionMap Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods | |
| Monoid hl => Convert (DelayedMerge hl) hl Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source # | |
| Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source # | |
| Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| 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.
Orphan instances
| Monoid Aspects Source # | |
| Monoid TokenBased Source # | |
Methods mempty :: TokenBased mappend :: TokenBased -> TokenBased -> TokenBased mconcat :: [TokenBased] -> TokenBased | |
| Semigroup Aspects Source # | |
| Semigroup DefinitionSite Source # | |
Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite # sconcat :: NonEmpty DefinitionSite -> DefinitionSite stimes :: Integral b => b -> DefinitionSite -> DefinitionSite | |
| Semigroup TokenBased Source # | |
Methods (<>) :: TokenBased -> TokenBased -> TokenBased # sconcat :: NonEmpty TokenBased -> TokenBased stimes :: Integral b => b -> TokenBased -> TokenBased | |
| NFData Aspect Source # | |
| NFData Aspects Source # | |
| NFData DefinitionSite Source # | |
Methods rnf :: DefinitionSite -> () | |
| NFData OtherAspect Source # | |
Methods rnf :: OtherAspect -> () | |