agda-language-server-0.2.6.3.0: An implementation of language server protocal (LSP) for Agda 2.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Render.Class

Synopsis

Documentation

class Render a where Source #

Typeclass for rendering Inlines

Minimal complete definition

Nothing

Methods

render :: a -> Inlines Source #

renderPrec :: Int -> a -> Inlines Source #

Instances

Instances details
Render Name Source #

Abstract

Instance details

Defined in Render.Name

Methods

render :: Name -> Inlines Source #

renderPrec :: Int -> Name -> Inlines Source #

Render QName Source # 
Instance details

Defined in Render.Name

Methods

render :: QName -> Inlines Source #

renderPrec :: Int -> QName -> Inlines Source #

Render Cohesion Source # 
Instance details

Defined in Render.Common

Methods

render :: Cohesion -> Inlines Source #

renderPrec :: Int -> Cohesion -> Inlines Source #

Render Fixity Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Fixity -> Inlines Source #

renderPrec :: Int -> Fixity -> Inlines Source #

Render Fixity' Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Fixity' -> Inlines Source #

renderPrec :: Int -> Fixity' -> Inlines Source #

Render Induction Source # 
Instance details

Defined in Render.Common

Methods

render :: Induction -> Inlines Source #

renderPrec :: Int -> Induction -> Inlines Source #

Render InteractionId Source #

InteractionId

Instance details

Defined in Render.Concrete

Methods

render :: InteractionId -> Inlines Source #

renderPrec :: Int -> InteractionId -> Inlines Source #

Render MetaId Source #

MetaId

Instance details

Defined in Render.Common

Methods

render :: MetaId -> Inlines Source #

renderPrec :: Int -> MetaId -> Inlines Source #

Render Modality Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Modality -> Inlines Source #

renderPrec :: Int -> Modality -> Inlines Source #

Render NameId Source #

NameId

Instance details

Defined in Render.Common

Methods

render :: NameId -> Inlines Source #

renderPrec :: Int -> NameId -> Inlines Source #

Render NotationPart Source # 
Instance details

Defined in Render.Concrete

Methods

render :: NotationPart -> Inlines Source #

renderPrec :: Int -> NotationPart -> Inlines Source #

Render ProblemId Source # 
Instance details

Defined in Render.TypeChecking

Methods

render :: ProblemId -> Inlines Source #

renderPrec :: Int -> ProblemId -> Inlines Source #

Render Quantity Source #

Quantity

Instance details

Defined in Render.Common

Methods

render :: Quantity -> Inlines Source #

renderPrec :: Int -> Quantity -> Inlines Source #

Render QωOrigin Source # 
Instance details

Defined in Render.Common

Methods

render :: QωOrigin -> Inlines Source #

renderPrec :: Int -> QωOrigin -> Inlines Source #

Render Relevance Source #

Relevance

Instance details

Defined in Render.Common

Methods

render :: Relevance -> Inlines Source #

renderPrec :: Int -> Relevance -> Inlines Source #

Render BoundName Source # 
Instance details

Defined in Render.Concrete

Methods

render :: BoundName -> Inlines Source #

renderPrec :: Int -> BoundName -> Inlines Source #

Render Declaration Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Declaration -> Inlines Source #

renderPrec :: Int -> Declaration -> Inlines Source #

Render DoStmt Source # 
Instance details

Defined in Render.Concrete

Methods

render :: DoStmt -> Inlines Source #

renderPrec :: Int -> DoStmt -> Inlines Source #

Render Expr Source #

Expression

Instance details

Defined in Render.Concrete

Methods

render :: Expr -> Inlines Source #

renderPrec :: Int -> Expr -> Inlines Source #

Render LHS Source # 
Instance details

Defined in Render.Concrete

Methods

render :: LHS -> Inlines Source #

renderPrec :: Int -> LHS -> Inlines Source #

Render LHSCore Source # 
Instance details

Defined in Render.Concrete

Methods

render :: LHSCore -> Inlines Source #

renderPrec :: Int -> LHSCore -> Inlines Source #

Render LamBinding Source #

LamBinding

Instance details

Defined in Render.Concrete

Methods

render :: LamBinding -> Inlines Source #

renderPrec :: Int -> LamBinding -> Inlines Source #

Render LamClause Source # 
Instance details

Defined in Render.Concrete

Methods

render :: LamClause -> Inlines Source #

renderPrec :: Int -> LamClause -> Inlines Source #

Render ModuleApplication Source # 
Instance details

Defined in Render.Concrete

Methods

render :: ModuleApplication -> Inlines Source #

renderPrec :: Int -> ModuleApplication -> Inlines Source #

Render ModuleAssignment Source # 
Instance details

Defined in Render.Concrete

Methods

render :: ModuleAssignment -> Inlines Source #

renderPrec :: Int -> ModuleAssignment -> Inlines Source #

Render OpenShortHand Source # 
Instance details

Defined in Render.Concrete

Methods

render :: OpenShortHand -> Inlines Source #

renderPrec :: Int -> OpenShortHand -> Inlines Source #

Render Pattern Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Pattern -> Inlines Source #

renderPrec :: Int -> Pattern -> Inlines Source #

Render Pragma Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Pragma -> Inlines Source #

renderPrec :: Int -> Pragma -> Inlines Source #

Render RHS Source # 
Instance details

Defined in Render.Concrete

Methods

render :: RHS -> Inlines Source #

renderPrec :: Int -> RHS -> Inlines Source #

Render TypedBinding Source #

TypedBinding

Instance details

Defined in Render.Concrete

Methods

render :: TypedBinding -> Inlines Source #

renderPrec :: Int -> TypedBinding -> Inlines Source #

Render WhereClause Source # 
Instance details

Defined in Render.Concrete

Methods

render :: WhereClause -> Inlines Source #

renderPrec :: Int -> WhereClause -> Inlines Source #

Render Name Source # 
Instance details

Defined in Render.Name

Methods

render :: Name -> Inlines Source #

renderPrec :: Int -> Name -> Inlines Source #

Render NamePart Source #

Concrete

Instance details

Defined in Render.Name

Methods

render :: NamePart -> Inlines Source #

renderPrec :: Int -> NamePart -> Inlines Source #

Render QName Source # 
Instance details

Defined in Render.Name

Methods

render :: QName -> Inlines Source #

renderPrec :: Int -> QName -> Inlines Source #

Render NamedBinding Source #

NamedBinding

Instance details

Defined in Render.Concrete

Methods

render :: NamedBinding -> Inlines Source #

renderPrec :: Int -> NamedBinding -> Inlines Source #

Render Tel Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Tel -> Inlines Source #

renderPrec :: Int -> Tel -> Inlines Source #

Render Clause Source # 
Instance details

Defined in Render.Internal

Methods

render :: Clause -> Inlines Source #

renderPrec :: Int -> Clause -> Inlines Source #

Render DBPatVar Source # 
Instance details

Defined in Render.Internal

Methods

render :: DBPatVar -> Inlines Source #

renderPrec :: Int -> DBPatVar -> Inlines Source #

Render Level Source # 
Instance details

Defined in Render.Internal

Methods

render :: Level -> Inlines Source #

renderPrec :: Int -> Level -> Inlines Source #

Render PlusLevel Source # 
Instance details

Defined in Render.Internal

Methods

render :: PlusLevel -> Inlines Source #

renderPrec :: Int -> PlusLevel -> Inlines Source #

Render Sort Source # 
Instance details

Defined in Render.Internal

Methods

render :: Sort -> Inlines Source #

renderPrec :: Int -> Sort -> Inlines Source #

Render Term Source #

Term

Instance details

Defined in Render.Internal

Methods

render :: Term -> Inlines Source #

renderPrec :: Int -> Term -> Inlines Source #

Render Type Source # 
Instance details

Defined in Render.Internal

Methods

render :: Type -> Inlines Source #

renderPrec :: Int -> Type -> Inlines Source #

Render Blocker Source # 
Instance details

Defined in Render.Internal

Methods

render :: Blocker -> Inlines Source #

renderPrec :: Int -> Blocker -> Inlines Source #

Render Literal Source #

Literal

Instance details

Defined in Render.Literal

Methods

render :: Literal -> Inlines Source #

renderPrec :: Int -> Literal -> Inlines Source #

Render IntervalWithoutFile Source # 
Instance details

Defined in Render.Position

Methods

render :: IntervalWithoutFile -> Inlines Source #

renderPrec :: Int -> IntervalWithoutFile -> Inlines Source #

Render PositionWithoutFile Source # 
Instance details

Defined in Render.Position

Methods

render :: PositionWithoutFile -> Inlines Source #

renderPrec :: Int -> PositionWithoutFile -> Inlines Source #

Render RangeFile Source # 
Instance details

Defined in Render.Position

Methods

render :: RangeFile -> Inlines Source #

renderPrec :: Int -> RangeFile -> Inlines Source #

Render Comparison Source # 
Instance details

Defined in Render.TypeChecking

Methods

render :: Comparison -> Inlines Source #

renderPrec :: Int -> Comparison -> Inlines Source #

Render NamedMeta Source # 
Instance details

Defined in Render.TypeChecking

Methods

render :: NamedMeta -> Inlines Source #

renderPrec :: Int -> NamedMeta -> Inlines Source #

Render Polarity Source # 
Instance details

Defined in Render.TypeChecking

Methods

render :: Polarity -> Inlines Source #

renderPrec :: Int -> Polarity -> Inlines Source #

Render Occurrence Source # 
Instance details

Defined in Render.TypeChecking

Methods

render :: Occurrence -> Inlines Source #

renderPrec :: Int -> Occurrence -> Inlines Source #

Render AbsolutePath Source # 
Instance details

Defined in Render.Position

Methods

render :: AbsolutePath -> Inlines Source #

renderPrec :: Int -> AbsolutePath -> Inlines Source #

Render CPUTime Source # 
Instance details

Defined in Render.Utils

Methods

render :: CPUTime -> Inlines Source #

renderPrec :: Int -> CPUTime -> Inlines Source #

Render Int32 Source # 
Instance details

Defined in Render.Class

Methods

render :: Int32 -> Inlines Source #

renderPrec :: Int -> Int32 -> Inlines Source #

Render Doc Source # 
Instance details

Defined in Render.Class

Methods

render :: Doc -> Inlines Source #

renderPrec :: Int -> Doc -> Inlines Source #

Render Integer Source # 
Instance details

Defined in Render.Class

Methods

render :: Integer -> Inlines Source #

renderPrec :: Int -> Integer -> Inlines Source #

Render Bool Source # 
Instance details

Defined in Render.Class

Methods

render :: Bool -> Inlines Source #

renderPrec :: Int -> Bool -> Inlines Source #

Render Int Source #

Other instances of Render

Instance details

Defined in Render.Class

Methods

render :: Int -> Inlines Source #

renderPrec :: Int -> Int -> Inlines Source #

Render a => Render (Arg a) Source #

Arg

Instance details

Defined in Render.Concrete

Methods

render :: Arg a -> Inlines Source #

renderPrec :: Int -> Arg a -> Inlines Source #

Render a => Render (MaybePlaceholder a) Source #

MaybePlaceholder

Instance details

Defined in Render.Concrete

Methods

render :: MaybePlaceholder a -> Inlines Source #

renderPrec :: Int -> MaybePlaceholder a -> Inlines Source #

Render a => Render (Ranged a) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Ranged a -> Inlines Source #

renderPrec :: Int -> Ranged a -> Inlines Source #

Render a => Render (WithHiding a) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: WithHiding a -> Inlines Source #

renderPrec :: Int -> WithHiding a -> Inlines Source #

Render a => Render (Binder' a) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Binder' a -> Inlines Source #

renderPrec :: Int -> Binder' a -> Inlines Source #

Render a => Render (FieldAssignment' a) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: FieldAssignment' a -> Inlines Source #

renderPrec :: Int -> FieldAssignment' a -> Inlines Source #

Render (OpApp Expr) Source #

OpApp

Instance details

Defined in Render.Concrete

Methods

render :: OpApp Expr -> Inlines Source #

renderPrec :: Int -> OpApp Expr -> Inlines Source #

Render a => Render (Pattern' a) Source # 
Instance details

Defined in Render.Internal

Methods

render :: Pattern' a -> Inlines Source #

renderPrec :: Int -> Pattern' a -> Inlines Source #

Render a => Render (Substitution' a) Source # 
Instance details

Defined in Render.Internal

Methods

render :: Substitution' a -> Inlines Source #

renderPrec :: Int -> Substitution' a -> Inlines Source #

Render a => Render (Tele (Dom a)) Source # 
Instance details

Defined in Render.Internal

Methods

render :: Tele (Dom a) -> Inlines Source #

renderPrec :: Int -> Tele (Dom a) -> Inlines Source #

Render tm => Render (Elim' tm) Source # 
Instance details

Defined in Render.Internal

Methods

render :: Elim' tm -> Inlines Source #

renderPrec :: Int -> Elim' tm -> Inlines Source #

Render a => Render (Interval' (Maybe a)) Source # 
Instance details

Defined in Render.Position

Methods

render :: Interval' (Maybe a) -> Inlines Source #

renderPrec :: Int -> Interval' (Maybe a) -> Inlines Source #

Render a => Render (Position' (Maybe a)) Source # 
Instance details

Defined in Render.Position

Methods

render :: Position' (Maybe a) -> Inlines Source #

renderPrec :: Int -> Position' (Maybe a) -> Inlines Source #

Render a => Render (Range' (Maybe a)) Source # 
Instance details

Defined in Render.Position

Methods

render :: Range' (Maybe a) -> Inlines Source #

renderPrec :: Int -> Range' (Maybe a) -> Inlines Source #

Render c => Render (IPBoundary' c) Source #

IPBoundary'

Instance details

Defined in Render.Interaction

Methods

render :: IPBoundary' c -> Inlines Source #

renderPrec :: Int -> IPBoundary' c -> Inlines Source #

Render a => Render (List1 a) Source # 
Instance details

Defined in Render.Class

Methods

render :: List1 a -> Inlines Source #

renderPrec :: Int -> List1 a -> Inlines Source #

Render a => Render (List2 a) Source # 
Instance details

Defined in Render.Class

Methods

render :: List2 a -> Inlines Source #

renderPrec :: Int -> List2 a -> Inlines Source #

Render a => Render [a] Source # 
Instance details

Defined in Render.Class

Methods

render :: [a] -> Inlines Source #

renderPrec :: Int -> [a] -> Inlines Source #

(Render a, Render b) => Render (OutputConstraint a b) Source #

OutputConstraint

Instance details

Defined in Render.Interaction

Methods

render :: OutputConstraint a b -> Inlines Source #

renderPrec :: Int -> OutputConstraint a b -> Inlines Source #

(Render a, Render b) => Render (OutputForm a b) Source #

OutputForm

Instance details

Defined in Render.Interaction

Methods

render :: OutputForm a b -> Inlines Source #

renderPrec :: Int -> OutputForm a b -> Inlines Source #

(Render a, Render b) => Render (ImportDirective' a b) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: ImportDirective' a b -> Inlines Source #

renderPrec :: Int -> ImportDirective' a b -> Inlines Source #

(Render a, Render b) => Render (ImportedName' a b) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: ImportedName' a b -> Inlines Source #

renderPrec :: Int -> ImportedName' a b -> Inlines Source #

Render e => Render (Named NamedName e) Source #

Named NamedName (Named_)

Instance details

Defined in Render.Concrete

Methods

render :: Named NamedName e -> Inlines Source #

renderPrec :: Int -> Named NamedName e -> Inlines Source #

(Render a, Render b) => Render (Renaming' a b) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Renaming' a b -> Inlines Source #

renderPrec :: Int -> Renaming' a b -> Inlines Source #

(Render a, Render b) => Render (Using' a b) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Using' a b -> Inlines Source #

renderPrec :: Int -> Using' a b -> Inlines Source #

(Render t, Render e) => Render (Dom' t e) Source # 
Instance details

Defined in Render.Internal

Methods

render :: Dom' t e -> Inlines Source #

renderPrec :: Int -> Dom' t e -> Inlines Source #

(Render a, Render b) => Render (Either a b) Source # 
Instance details

Defined in Render.Concrete

Methods

render :: Either a b -> Inlines Source #

renderPrec :: Int -> Either a b -> Inlines Source #

(Render p, Render e) => Render (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Render.Common

Methods

render :: RewriteEqn' qn nm p e -> Inlines Source #

renderPrec :: Int -> RewriteEqn' qn nm p e -> Inlines Source #

renderM :: (Applicative m, Render a) => a -> m Inlines Source #

Rendering undersome context class RenderTCM a where renderTCM :: a -> Agda.TCM Inlines

Simply "pure . render"

renderP :: (Applicative m, Pretty a) => a -> m Inlines Source #

Render instances of Pretty

renderA :: (Render c, ToConcrete a, ConOfAbs a ~ c) => a -> TCM Inlines Source #

like prettyA

renderATop :: (Render c, ToConcrete a, ConOfAbs a ~ c) => a -> TCM Inlines Source #

like prettyATop