@@ -1210,6 +1210,8 @@ pprintPTerm impl bnd = prettySe 10 bnd
1211 slist' p bnd (PApp _ (PRef _ nil) _)
1211 slist' p bnd (PApp _ (PRef _ nil) _)
1212 | not impl && nsroot nil == sUN "Nil" = Just []
1212 | not impl && nsroot nil == sUN "Nil" = Just []
1213+ slist' p bnd (PRef _ nil)
1214+ | not impl && nsroot nil == sUN "Nil" = Just []
1213 slist' p bnd (PApp _ (PRef _ cons) args)
1215 slist' p bnd (PApp _ (PRef _ cons) args)
1214 | nsroot cons == sUN "::",
1216 | nsroot cons == sUN "::",
1215 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1217 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
@@ -1219,14 +1221,16 @@ pprintPTerm impl bnd = prettySe 10 bnd
1220 isImp (PImp {}) = True
1222 isImp (PImp {}) = True
1221 isImp _ = False
1223 isImp _ = False
1222− slist' _ _ _ = Nothing
1224+ slist' _ _ tm = Nothing
1224 slist p bnd e | Just es <- slist' p bnd e = Just $
1226 slist p bnd e | Just es <- slist' p bnd e = Just $
1225 case es of [] -> annotate AnnConstData $ text "[]"
1227 case es of [] -> annotate AnnConstData $ text "[]"
1226− [x] -> enclose left
1228+ [x] -> enclose left right . group $
1228− (prettySe p bnd x)
1229+ prettySe p bnd x
1229− xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs
1230+ xs -> (enclose left right .
1231+ align . group . vsep .
1233+ map (prettySe p bnd)) xs
1230 where left = (annotate AnnConstData (text "["))
1234 where left = (annotate AnnConstData (text "["))
1231 right = (annotate AnnConstData (text "]"))
1235 right = (annotate AnnConstData (text "]"))
1232 comma = (annotate AnnConstData (text ","))
1236 comma = (annotate AnnConstData (text ","))