Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.DocTree

Description

A simple document tree to render Doc ann but preserve annotations.

DocTree and renderToTree' originally taken from https://github.com/plt-amy/agda/blob/9fd50b883f14a05792ed79a0b693fbecb2165bf5/src/full/Agda/LSP/Output.hs but rewritten to encode more invariants.

Synopsis

Documentation

data DocTree ann Source #

A rendered document with annotations from type ann.

Constructors

Node ann [DocTree ann]

Stuff annotated by ann.

Text Text

Atom.

Instances

Instances details
EncodeTCM DocTree Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: DocTree -> TCM Value Source #

ToJSON DocTree Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

toJSON :: DocTree -> Value #

toEncoding :: DocTree -> Encoding #

toJSONList :: [DocTree] -> Value #

toEncodingList :: [DocTree] -> Encoding #

omitField :: DocTree -> Bool #

a ~ Aspects => Pretty (DocTree a) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: DocTree a -> Doc Source #

prettyPrec :: Int -> DocTree a -> Doc Source #

prettyList :: [DocTree a] -> Doc Source #

EmbPrj a => EmbPrj (DocTree a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.General

Methods

icode :: DocTree a -> S Word32 Source #

icod_ :: DocTree a -> S Word32 Source #

value :: Word32 -> R (DocTree a) Source #

Null (DocTree ann) Source # 
Instance details

Defined in Agda.Utils.DocTree

Methods

empty :: DocTree ann Source #

null :: DocTree ann -> Bool Source #

NFData ann => NFData (DocTree ann) Source # 
Instance details

Defined in Agda.Utils.DocTree

Methods

rnf :: DocTree ann -> () #

Generic (DocTree ann) Source # 
Instance details

Defined in Agda.Utils.DocTree

Associated Types

type Rep (DocTree ann) 
Instance details

Defined in Agda.Utils.DocTree

type Rep (DocTree ann) = D1 ('MetaData "DocTree" "Agda.Utils.DocTree" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "Node" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DocTree ann])) :+: C1 ('MetaCons "Text" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

Methods

from :: DocTree ann -> Rep (DocTree ann) x #

to :: Rep (DocTree ann) x -> DocTree ann #

Show ann => Show (DocTree ann) Source # 
Instance details

Defined in Agda.Utils.DocTree

Methods

showsPrec :: Int -> DocTree ann -> ShowS #

show :: DocTree ann -> String #

showList :: [DocTree ann] -> ShowS #

type Rep (DocTree ann) Source # 
Instance details

Defined in Agda.Utils.DocTree

type Rep (DocTree ann) = D1 ('MetaData "DocTree" "Agda.Utils.DocTree" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "Node" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DocTree ann])) :+: C1 ('MetaCons "Text" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

prettyDocTree :: DocTree ann -> Doc ann Source #

renderToTree :: Null ann => Doc ann -> DocTree ann Source #

Render a Doc ann to a DocTree ann using standard layout parameters.

renderToTree' :: Null ann => Width -> Fill -> Doc ann -> DocTree ann Source #

Render a Doc ann to a DocTree ann with the given layout parameters. E.g. width=100 fill=1.5.

renderTree' :: forall ann t. Monoid t => (Text -> t) -> (ann -> t -> t) -> DocTree ann -> t Source #

Generic DocTree linearization.

treeToText :: (ann -> Text -> Text) -> DocTree ann -> Text Source #

Linearize a DocTree to Text with the given Text-rendering of the annotations.

treeToTextNoAnn :: DocTree ann -> Text Source #

Linearize a DocTree to Text dropping all annotations.

treeToTextWithAnn :: (Monoid ann, Null ann) => DocTree ann -> (Text, RangeMap ann) Source #