@@ -1433,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1434 prettySe p bnd (PLam fc n ty sc) =
1434 prettySe p bnd (PLam fc n ty sc) =
1435 bracket p startPrec . group . align . hang 2 $
1435 bracket p startPrec . group . align . hang 2 $
1436− text "\\" <> bindingOf n False <+> text "=>" <$>
1436+ text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1437 prettySe startPrec ((n, False):bnd) sc
1437 prettySe startPrec ((n, False):bnd) sc
1438 prettySe p bnd (PLet fc n ty v sc) =
1438 prettySe p bnd (PLet fc n ty v sc) =
1439 bracket p startPrec . group . align $
1439 bracket p startPrec . group . align $
1440− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1440+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1442 prettySe p bnd (PPi (Exp l s _) n ty sc)
1442 prettySe p bnd (PPi (Exp l s _) n ty sc)
1443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1444 bracket p startPrec . group $
1444 bracket p startPrec . group $
1445− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1445+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1447 | otherwise =
1447 | otherwise =
1448 bracket p startPrec . group $
1448 bracket p startPrec . group $
@@ -1455,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1456 | ppopt_impl ppo =
1456 | ppopt_impl ppo =
1457 bracket p startPrec $
1457 bracket p startPrec $
1458− lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1458+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1460 | otherwise = prettySe startPrec ((n, True):bnd) sc
1460 | otherwise = prettySe startPrec ((n, True):bnd) sc
@@ -1612,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1613 prettySe p bnd _ = text "missing pretty-printer for term"
1613 prettySe p bnd _ = text "missing pretty-printer for term"
1615+ prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1616+ prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1617+ where display (UN n) = T.unpack n
1618+ display (MN _ n) = T.unpack n
1619+ -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1620+ display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1615 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1623 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1616 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1624 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1617 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1625 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm