@@ -342,13 +342,24 @@ pprintErr' i (ReflectionFailed msg err) =
342342pprintErr' i (ElabDebug msg tm holes) =
343343 text "Elaboration halted." <>
344344 maybe empty (indented . text) msg <> line <>
345− text "Term: " <> pprintTerm' i [] (delab i tm) <> line <>
345+ text "Term: " <> indented (pprintTerm' i [] (delab i tm)) <> line <>
346346 text "Holes:" <>
347− (indented . vsep . flip map holes)
348− (\(hn, goal, env) ->
349− vsep (flip map env (\(n, b) -> annName' n (show n) <+> text ":" <+> pprintTerm' i [] (delab i (binderTy b)))) <> -- TODO: nested binders
350− line <> text "----------------------------------" <> line <>
351− annName' hn (show hn) <+> text ":" <+> pprintTerm' i (zip (map fst env) (repeat True)) (delab i goal) <> line)
347+ indented (vsep (map ppHole holes))
348+
349+ where ppHole :: (Name, Type, Env) -> Doc OutputAnnotation
350+ ppHole (hn, goal, env) =
351+ ppAssumptions [] (reverse env) <>
352+ text "----------------------------------" <> line <>
353+ bindingOf hn False <+> text ":" <+>
354+ pprintTerm' i (zip (map fst env) (repeat False)) (delab i goal) <> line
355+ ppAssumptions :: [Name] -> Env -> Doc OutputAnnotation
356+ ppAssumptions ns [] = empty
357+ ppAssumptions ns ((n, b) : rest) =
358+ bindingOf n False <+>
359+ text ":" <+>
360+ pprintTerm' i (zip ns (repeat False)) (delab i (binderTy b)) <>
361+ line <>
362+ ppAssumptions (n:ns) rest
352363
353364-- | Make sure the machine invented names are shown helpfully to the user, so
354365-- that any names which differ internally also differ visibly