@@ -26,6 +26,7 @@ import qualified Control.Monad.Trans.Class as Trans (lift)
2626
2727import Data.Data (Data)
2828import Data.Function (on)
29+import Data.Generics.Uniplate.Data (universe)
2930import Data.List hiding (group)
3031import Data.Char
3132import qualified Data.Map.Strict as M
@@ -1375,6 +1376,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
13751376 where
13761377 startPrec = 0
13771378 funcAppPrec = 10
1379+
13781380 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
13791381 prettySe p bnd (PQuote r) =
13801382 text "![" <> pretty r <> text "]"
@@ -1640,6 +1642,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16401642 getFixity :: String -> Maybe Fixity
16411643 getFixity = flip M.lookup fixities
16421644
1645+-- | Determine whether a name was the one inserted for a hole or
1646+-- guess by the delaborator
1647+isHoleName :: Name -> Bool
1648+isHoleName (UN n) = n == T.pack "[__]"
1649+isHoleName _ = False
1650+
1651+-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1652+containsHole :: PTerm -> Bool
1653+containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]
1654+
16431655-- | Pretty-printer helper for the binding site of a name
16441656bindingOf :: Name -- ^^ the bound name
16451657 -> Bool -- ^^ whether the name is implicit
@@ -1727,6 +1739,8 @@ getShowArgs :: [PArg] -> [PArg]
17271739getShowArgs [] = []
17281740getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
17291741getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1742+ | PImp _ _ _ _ tm <- e
1743+ , containsHole tm = e : getShowArgs xs
17301744getShowArgs (_ : xs) = getShowArgs xs
17311745
17321746getConsts :: [PArg] -> [PTerm]