git.iko.soy/Idris-dev
on master help sign in
Failing 'focus' should be harmless

Sometimes there's a focus where everything is done because unification has solved things, and if it doesn't fail harmlessly then there'll be a meaningless "Nothing to fill in" error. Fixes #2342

commit268459cf99c5a0a3fd14f0f76cc8633b429955f8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 Jul 2015, 17:35 (11 years ago) parent49af6f9
1 file changed+4−1
compare with master
unifiedsplit
src/Idris/Core/ProofState.hs+4−1
src/Idris/Core/ProofState.hs+4−1
@@ -1025,7 +1025,10 @@ processTactic (MatchProblems all) ps
10251025 holes = holes ps \\ (map fst ns'') }, plog ps)
10261026processTactic t ps
10271027 = case holes ps of
1028− [] -> fail "Nothing to fill in."
1028+ [] -> case t of
1029+ Focus _ -> return (ps, "") -- harmless to refocus when done, since
1030+ -- 'focus' doesn't fail
1031+ _ -> fail $ "Nothing to fill in."
10291032 (h:_) -> do ps' <- execStateT (process t h) ps
10301033 let (ns_in, probs')
10311034 = case solved ps' of