@@ -1131,17 +1131,28 @@ pprintPTerm impl bnd = prettySe 10 bnd
1131 bracket p 2 $
1131 bracket p 2 $
1132 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1132 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1133 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1133 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1134− prettySe p bnd (PApp _ (PRef _ f) [])
1134+ prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1135+ | UN nm <- basename f
1136+ , not impl && null (getExps args) = if isAlpha (thead nm)
1137+ then prettyName impl bnd f
1138+ else enclose lparen rparen $
1135− | not impl = prettyName impl bnd f
1139+ prettyName impl bnd f
1136 prettySe p bnd (PAppBind _ (PRef _ f) [])
1140 prettySe p bnd (PAppBind _ (PRef _ f) [])
1137 | not impl = text "!" <> prettyName impl bnd f
1141 | not impl = text "!" <> prettyName impl bnd f
1138 prettySe p bnd (PApp _ (PRef _ op) args)
1142 prettySe p bnd (PApp _ (PRef _ op) args)
1139 | UN nm <- basename op
1143 | UN nm <- basename op
1140 , not (tnull nm) &&
1144 , not (tnull nm) &&
1141− length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
1145+ (not impl) && (not $ isAlpha (thead nm)) =
1142− let [l, r] = getExps args in
1146+ case getExps args of
1147+ [] -> enclose lparen rparen opName
1148+ [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))
1149+ [l,r] -> bracket p 1 $ inFix l r
1143− bracket p 1 . align . group $
1150+ (l:r:rest) -> bracket p 1 $
1151+ enclose lparen rparen (inFix l r) <+>
1152+ align (group (vsep (map (prettyArgSe bnd) rest)))
1144− (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)
1153+ where opName = prettyName impl bnd op
1154+ inFix l r = align . group $
1155+ (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)
1145 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1156 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1146 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1157 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1147 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1158 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))