It is now an error to focus on nonexisting holes in Elab scripts
This makes subtle bugs more obvious.
commit82c273563757deee4954e50bbc10bd92e9b98b64
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateWed 12 Aug 2015, 18:07 (11 years ago)
parent603b06c
src/Idris/Elab/Term.hs+4−2
@@ -2051,8 +2051,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20512051 returnUnit
20522052 | n == tacN "prim__Focus", [what] <- args
20532053 = do n' <- reifyTTName what
2054− focus n'
2055− returnUnit
2054+ hs <- get_holes
2055+ if elem n' hs
2056+ then focus n' >> returnUnit
2057+ else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
20562058 | n == tacN "prim__Unfocus", [what] <- args
20572059 = do n' <- reifyTTName what
20582060 movelast n'