Skip to content

Commit ec16e50

Browse files
committed
docs: for Show.Lines.align
1 parent b945134 commit ec16e50

1 file changed

Lines changed: 15 additions & 1 deletion

File tree

src/Vatras/Show/Lines.agda

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,22 @@ stringLength line = List.sum (List.map charWidth (Data.String.toList line))
5353
length : Line
5454
length line = stringLength (content line)
5555

56+
-- Align the given line to have the given width.
57+
-- This will add spaces before and/or after the line depending on the line's alignment.
58+
-- also see: Data.String.Base.fromAlignment
5659
align : Line Line
57-
align width line = manipulate (fromAlignment (alignment line) (width ∸ (length line ∸ Data.String.length (content line)))) line
60+
align width line =
61+
manipulate
62+
(fromAlignment
63+
(alignment line)
64+
-- We use the fromAlignment function of the standard library,
65+
-- which considers all characters to have width 1.
66+
-- If the line contains characters with width > 1 (e.g., emojis),
67+
-- then fromAlignment would add too much padding. So we have to
68+
-- decrease the padding value accordingly.
69+
(width ∸ (length line ∸ Data.String.length (content line)))
70+
)
71+
line
5872

5973
{-|
6074
Lines monad.

0 commit comments

Comments
 (0)