@@ -16,7 +16,7 @@ data Doc : Type where
17 Cat : (x : Doc) -> (y : Doc) -> Doc
17 Cat : (x : Doc) -> (y : Doc) -> Doc
18 Nest : (lvl : Int) -> (x : Doc) -> Doc
18 Nest : (lvl : Int) -> (x : Doc) -> Doc
19− Union : (x : Doc) -> (y : Doc) -> Doc
19+ Union : (x : Doc) -> (y : Lazy Doc) -> Doc
21 Column : (f : Int -> Doc) -> Doc
21 Column : (f : Int -> Doc) -> Doc
22 Nesting : (f : Int -> Doc) -> Doc
22 Nesting : (f : Int -> Doc) -> Doc
@@ -162,11 +162,12 @@ render rfrac w doc = best w 0 0 doc (const Empty)
162 nicest : (lvl : Int)
162 nicest : (lvl : Int)
163 -> (col : Int)
163 -> (col : Int)
164 -> (x : PrettyDoc)
164 -> (x : PrettyDoc)
165− -> (y : PrettyDoc)
165+ -> (y : Lazy PrettyDoc)
166 -> PrettyDoc
166 -> PrettyDoc
167 nicest n k x y =
167 nicest n k x y =
168− let width = min (w - k) (rwidth - k + n)
168+ if fits (min (w - k) (rwidth - k + n)) x
169− in if fits width x then x else y
169+ then x
171 best : (lvl : Int)
172 best : (lvl : Int)
172 -> (col : Int)
173 -> (col : Int)