mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
32 lines
943 B
Idris
32 lines
943 B
Idris
module Text.PrettyPrint.Prettyprinter.Util
|
|
|
|
import Data.List
|
|
import Data.Strings
|
|
import Text.PrettyPrint.Prettyprinter.Doc
|
|
import Text.PrettyPrint.Prettyprinter.Render.String
|
|
|
|
%default total
|
|
|
|
||| Split an input into word-sized `Doc`.
|
|
export
|
|
words : String -> List (Doc ann)
|
|
words s = map pretty $ map pack (helper (unpack s))
|
|
where
|
|
helper : List Char -> List (List Char)
|
|
helper s =
|
|
case dropWhile isSpace s of
|
|
[] => []
|
|
s' => let (w, s'') = break isSpace s' in
|
|
w :: helper (assert_smaller s s'')
|
|
|
|
||| Insert soft linebreaks between words, so that text is broken into multiple
|
|
||| lines when it exceeds the available width.
|
|
export
|
|
reflow : String -> Doc ann
|
|
reflow = fillSep . words
|
|
|
|
||| Renders a document with a certain width.
|
|
export
|
|
putDocW : Nat -> Doc ann -> IO ()
|
|
putDocW w = renderIO . layoutPretty (record { layoutPageWidth = AvailablePerLine (cast w) 1 } defaultLayoutOptions)
|