Cornelis.Pretty

Documentation

data HighlightGroup

Custom highlight groups set by the plugin.

These groups linked to Neovim default highlight groups in syntax/agda.vim.

The suffix after CornelisXXX matches the names as returned by Agda, contained in hl_atoms. How these names are generated is not documented on Agda's side, but the implementation can be found at toAtoms. The correspoding Agda types are found in Precise.

NOTE: * When modifying this type, remember to sync the changes to syntax/agda.vim * This list of highlight groups does not yet cover all variants returned by Agda

Constructors

CornelisError

InfoWin highlight group of error messages

CornelisErrorWarning

InfoWin highlight group of warnings considered fatal

CornelisWarn

InfoWin highlight group of warnings

CornelisTitle

InfoWin highlight of section titles

CornelisName

InfoWin highlight of names in context

CornelisHole

An open hole ({! ... !} and ?)

CornelisUnsolvedMeta

An unresolved meta variable

CornelisUnsolvedConstraint

An unresolved constraint

CornelisKeyword

An Agda keywords (where, let, etc.)

CornelisSymbol

A symbol, not part of an identifier (=, :, {, etc.)

CornelisType

A datatype (Nat, Bool, etc.)

CornelisPrimitiveType

A primitive/builtin Agda type

CornelisRecord

A datatype, defined as a record

CornelisFunction

A function, e.g. a top-level declaration

CornelisArgument

The name of an (implicit) argument, i.e. Foo {bar = 42}

CornelisBound

A bound identifier, e.g. a variable in a pattern clause or a module parameter

CornelisOperator

A mixfix operator, e.g. x ∷ xs.

CornelisField

Field of a record definition

CornelisGeneralizable

A generalizable variable, defined for example in a variable block

CornelisMacro

A macro, defined in a macro block

CornelisInductiveConstructor

A constructor of an inductive data type (e.g. data Foo ...)

CornelisCoinductiveConstructor

A constructor for a coinductive datatype, i.e. a record marked coinductive

CornelisNumber

A number literal

CornelisComment

A comment

CornelisString

A string literal

CornelisCatchAllClause

"Catch-all clause". Some sort of fallback; not exactly clear where this is used

CornelisTypeChecks

A location being type-checked right now

CornelisModule

A module name, e.g. in a module block or an import

CornelisPostulate

A term, defined in a postulate block

CornelisPrimitive

An Agda primitive, e.g. Set

CornelisPragma

The argument to a pragma, e.g. {-# OPTIONS --foo -#}

Instances

Bounded HighlightGroup

Defined in Cornelis.Pretty

Methods

minBound :: HighlightGroup

maxBound :: HighlightGroup

Enum HighlightGroup

Defined in Cornelis.Pretty

Methods

succ :: HighlightGroup -> HighlightGroup

pred :: HighlightGroup -> HighlightGroup

toEnum :: Int -> HighlightGroup

fromEnum :: HighlightGroup -> Int

enumFrom :: HighlightGroup -> [HighlightGroup]

enumFromThen :: HighlightGroup -> HighlightGroup -> [HighlightGroup]

enumFromTo :: HighlightGroup -> HighlightGroup -> [HighlightGroup]

enumFromThenTo :: HighlightGroup -> HighlightGroup -> HighlightGroup -> [HighlightGroup]

Read HighlightGroup

Defined in Cornelis.Pretty

Methods

readsPrec :: Int -> ReadS HighlightGroup

readList :: ReadS [HighlightGroup]

readPrec :: ReadPrec HighlightGroup

readListPrec :: ReadPrec [HighlightGroup]

Show HighlightGroup

Defined in Cornelis.Pretty

Methods

showsPrec :: Int -> HighlightGroup -> ShowS

show :: HighlightGroup -> String

showList :: [HighlightGroup] -> ShowS

Eq HighlightGroup

Defined in Cornelis.Pretty

Methods

(==) :: HighlightGroup -> HighlightGroup -> Bool

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

Ord HighlightGroup

Defined in Cornelis.Pretty

Methods

compare :: HighlightGroup -> HighlightGroup -> Ordering

(<) :: HighlightGroup -> HighlightGroup -> Bool

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

(>) :: HighlightGroup -> HighlightGroup -> Bool

(>=) :: HighlightGroup -> HighlightGroup -> Bool

max :: HighlightGroup -> HighlightGroup -> HighlightGroup

min :: HighlightGroup -> HighlightGroup -> HighlightGroup

priority :: HighlightGroup -> Int64

Priority of the HighlightGroup. See `:h vim.highlight.priorities` for more information.

100 is the default syntax highlighting priority, while 150 is reserved for diagnostics.

atomToHlGroup :: Text -> Maybe HighlightGroup

data InfoHighlight a

Constructors

InfoHighlight

Fields

• ihl_start :: (Int64, Int64)
• ihl_end :: a
• ihl_group :: HighlightGroup

Instances

Functor InfoHighlight

Defined in Cornelis.Pretty

Methods

fmap :: (a -> b) -> InfoHighlight a -> InfoHighlight b

(<$) :: a -> InfoHighlight b -> InfoHighlight a

Show a => Show (InfoHighlight a)

Defined in Cornelis.Pretty

Methods

showsPrec :: Int -> InfoHighlight a -> ShowS

show :: InfoHighlight a -> String

showList :: [InfoHighlight a] -> ShowS

Eq a => Eq (InfoHighlight a)

Defined in Cornelis.Pretty

Methods

(==) :: InfoHighlight a -> InfoHighlight a -> Bool

(/=) :: InfoHighlight a -> InfoHighlight a -> Bool

Ord a => Ord (InfoHighlight a)

Defined in Cornelis.Pretty

Methods

compare :: InfoHighlight a -> InfoHighlight a -> Ordering

(<) :: InfoHighlight a -> InfoHighlight a -> Bool

(<=) :: InfoHighlight a -> InfoHighlight a -> Bool

(>) :: InfoHighlight a -> InfoHighlight a -> Bool

(>=) :: InfoHighlight a -> InfoHighlight a -> Bool

max :: InfoHighlight a -> InfoHighlight a -> InfoHighlight a

min :: InfoHighlight a -> InfoHighlight a -> InfoHighlight a

spanInfoHighlights :: InfoHighlight (Int64, Int64) -> [InfoHighlight Int64]

renderWithHlGroups :: SimpleDocStream HighlightGroup -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)

prettyType :: Type -> Doc HighlightGroup

groupScopeSet :: [InScope] -> [[InScope]]

prettyGoals :: DisplayInfo -> Doc HighlightGroup

prettyInterval :: AgdaInterval -> Doc HighlightGroup

prettyPoint :: AgdaPos -> Doc HighlightGroup

isEmpty :: Doc HighlightGroup -> Bool

section :: Doc HighlightGroup -> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup

prettyName :: Text -> Doc HighlightGroup

prettyVisibleName :: Bool -> Text -> Doc HighlightGroup

prettyInScope :: InScope -> Doc HighlightGroup

prettyInScopeSet :: [InScope] -> Doc HighlightGroup

prettyManyGoals :: [InScope] -> Type -> Doc HighlightGroup

prettyGoal :: GoalInfo Text -> Doc HighlightGroup

prettyError :: Message -> Doc HighlightGroup