From 8822040f37626a69db8c0caa1c30ac34f841300f Mon Sep 17 00:00:00 2001
From: Justus Matthiesen <mail@justusmatthiesen.com>
Date: Wed, 1 Nov 2023 15:01:54 +0000
Subject: [PATCH] [ new ] `replicateChar`, an analogue to `spaces` but for
 arbitrary `Char`s

---
 .../Text/PrettyPrint/Prettyprinter/Doc.idr    | 22 ++++++++++++++-----
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
index c2d470a57..d74599e3f 100644
--- a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
+++ b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
@@ -10,9 +10,13 @@ import Libraries.Data.String.Extra
 
 %default total
 
+export
+textReplicateChar : Int -> Char -> String
+textReplicateChar n = String.replicate (integerToNat $ cast n)
+
 export
 textSpaces : Int -> String
-textSpaces n = String.replicate (integerToNat $ cast n) ' '
+textSpaces n = textReplicateChar n ' '
 
 ||| Maximum number of characters that fit in one line.
 public export
@@ -104,14 +108,20 @@ export
 hang : Int -> Doc ann -> Doc ann
 hang i d = align (nest i d)
 
+||| Repeat character `n` times.
+export
+replicateChar : (n : Int) -> Char -> Doc ann
+replicateChar n c =
+  if n <= 0
+     then Empty
+     else if n == 1
+             then Chara c
+             else Text n (textReplicateChar n c)
+
 ||| Insert a number of spaces.
 export
 spaces : Int -> Doc ann
-spaces n = if n <= 0
-              then Empty
-              else if n == 1
-                      then Chara ' '
-                      else Text n (textSpaces n)
+spaces n = replicateChar n ' '
 
 ||| Indents a document with `i` spaces, starting from the current cursor position.
 export