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