0 | module Text.PrettyPrint.Prettyprinter.Util
 1 |
 2 | import Data.List
 3 | import Text.PrettyPrint.Prettyprinter.Doc
 4 | import Text.PrettyPrint.Prettyprinter.Render.String
 5 |
 6 | %default total
 7 |
 8 | ||| Split an input into word-sized `Doc`.
 9 | export
10 | words : String -> List (Doc ann)
11 | words s = map pretty $ map pack (helper (unpack s))
12 |   where
13 |     helper : List Char -> List (List Char)
14 |     helper s =
15 |       case dropWhile isSpace s of
16 |            [] => []
17 |            s' => let (w, s'') = break isSpace s' in
18 |                      w :: helper (assert_smaller s s'')
19 |
20 | ||| Insert soft linebreaks between words, so that text is broken into multiple
21 | ||| lines when it exceeds the available width.
22 | export
23 | reflow : String -> Doc ann
24 | reflow = fillSep . words
25 |
26 | ||| Renders a document with a certain width.
27 | export
28 | putDocW : Nat -> Doc ann -> IO ()
29 | putDocW w = renderIO . layoutPretty ({ layoutPageWidth := AvailablePerLine (cast w) 1 } defaultLayoutOptions)
30 |