git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2226 from david-christiansen/wip/tactical

Minor UI bug fixes in preparation for talk

commite2915e78641791d7a9050e3143a7b03202cda313 authorDavid Christiansen <david@davidchristiansen.dk> dateSat 2 May 2015, 00:11 (11 years ago) parent4c1a68d8f73696
2 files changed+5−4
compare with master
unifiedsplit
src/Idris/CaseSplit.hs+1−1 src/Idris/Delaborate.hs+4−3
src/Idris/CaseSplit.hs+1−1
@@ -69,7 +69,7 @@ split n t'
6969 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
7070 let ctxt = tt_ctxt ist
7171 case lookup n pats of
72− Nothing -> fail $ show n ++ " is not a pattern variable"
72+ Nothing -> ifail $ show n ++ " is not a pattern variable"
7373 Just ty ->
7474 do let splits = findPats ist ty
7575 iLOG ("New patterns " ++ showSep ", "
src/Idris/Delaborate.hs+4−3
@@ -382,10 +382,11 @@ pprintErr' i (ReflectionFailed msg err) =
382382 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
383383pprintErr' i (ElabScriptDebug msg tm holes) =
384384 text "Elaboration halted." <>
385− maybe empty (indented . text) msg <> line <>
386− text "Term: " <> indented (pprintTT [] tm) <> line <>
385+ maybe empty (indented . text) msg <>
386+ line <> line <>
387387 text "Holes:" <>
388− indented (vsep (map ppHole holes))
388+ indented (vsep (map ppHole holes)) <> line <> line <>
389+ text "Term: " <> indented (pprintTT [] tm)
389390
390391 where ppHole :: (Name, Type, Env) -> Doc OutputAnnotation
391392 ppHole (hn, goal, env) =