@@ -26,6 +26,7 @@ import qualified Control.Monad.Trans.Class as Trans (lift)
27import Data.Data (Data)
27import Data.Data (Data)
28import Data.Function (on)
28import Data.Function (on)
29+import Data.Generics.Uniplate.Data (universe)
29import Data.List hiding (group)
30import Data.List hiding (group)
30import Data.Char
31import Data.Char
31import qualified Data.Map.Strict as M
32import qualified Data.Map.Strict as M
@@ -1375,6 +1376,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1376 startPrec = 0
1377 startPrec = 0
1377 funcAppPrec = 10
1378 funcAppPrec = 10
1378 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1380 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1379 prettySe p bnd (PQuote r) =
1381 prettySe p bnd (PQuote r) =
1380 text "![" <> pretty r <> text "]"
1382 text "![" <> pretty r <> text "]"
@@ -1640,6 +1642,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1640 getFixity :: String -> Maybe Fixity
1642 getFixity :: String -> Maybe Fixity
1641 getFixity = flip M.lookup fixities
1643 getFixity = flip M.lookup fixities
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
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]
1643-- | Pretty-printer helper for the binding site of a name
1655-- | Pretty-printer helper for the binding site of a name
1644bindingOf :: Name -- ^^ the bound name
1656bindingOf :: Name -- ^^ the bound name
1645 -> Bool -- ^^ whether the name is implicit
1657 -> Bool -- ^^ whether the name is implicit
@@ -1727,6 +1739,8 @@ getShowArgs :: [PArg] -> [PArg]
1727getShowArgs [] = []
1739getShowArgs [] = []
1728getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1740getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1729getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1741getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1742+ | PImp _ _ _ _ tm <- e
1743+ , containsHole tm = e : getShowArgs xs
1730getShowArgs (_ : xs) = getShowArgs xs
1744getShowArgs (_ : xs) = getShowArgs xs
1732getConsts :: [PArg] -> [PTerm]
1746getConsts :: [PArg] -> [PTerm]