28ffcf8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Correctly pretty-print no-argument Nil

Previously, when the Nil constructor took no arguments (as was the case with HVect), it was not shown in sugared syntax in the pretty-printer. Fixes #820.

commit28ffcf824723d686f5b3c45047c8c1ada5714300 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 2 Feb 2014, 22:00 (13 years ago) parent4257d64

1 file changed+9−5

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+9−5

src/Idris/AbsSyntaxTree.hs+9−5

@@ -1210,6 +1210,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

12101210

12111211 slist' p bnd (PApp _ (PRef _ nil) _)

12121212 | not impl && nsroot nil == sUN "Nil" = Just []

1213+ slist' p bnd (PRef _ nil)

1214+ | not impl && nsroot nil == sUN "Nil" = Just []

12131215 slist' p bnd (PApp _ (PRef _ cons) args)

12141216 | nsroot cons == sUN "::",

12151217 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

@@ -1219,14 +1221,16 @@ pprintPTerm impl bnd = prettySe 10 bnd

12191221 where

12201222 isImp (PImp {}) = True

12211223 isImp _ = False

1222− slist' _ _ _ = Nothing

1224+ slist' _ _ tm = Nothing

12231225

12241226 slist p bnd e | Just es <- slist' p bnd e = Just $

12251227 case es of [] -> annotate AnnConstData $ text "[]"

1226− [x] -> enclose left

1227− right

1228− (prettySe p bnd x)

1229− xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs

1228+ [x] -> enclose left right . group $

1229+ prettySe p bnd x

1230+ xs -> (enclose left right .

1231+ align . group . vsep .

1232+ punctuate comma .

1233+ map (prettySe p bnd)) xs

12301234 where left = (annotate AnnConstData (text "["))

12311235 right = (annotate AnnConstData (text "]"))

12321236 comma = (annotate AnnConstData (text ","))