@@ -2051,8 +2051,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2051 returnUnit
2051 returnUnit
2052 | n == tacN "prim__Focus", [what] <- args
2052 | n == tacN "prim__Focus", [what] <- args
2053 = do n' <- reifyTTName what
2053 = do n' <- reifyTTName what
2054− focus n'
2054+ hs <- get_holes
2055− returnUnit
2056+ then focus n' >> returnUnit
2057+ else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
2056 | n == tacN "prim__Unfocus", [what] <- args
2058 | n == tacN "prim__Unfocus", [what] <- args
2057 = do n' <- reifyTTName what
2059 = do n' <- reifyTTName what
2058 movelast n'
2060 movelast n'