Don't block under Delay in repl evaluation

Fixes #2063
idris-lang · Mar 30, 2015 · 78a55ab · 78a55ab
1 parent a0725d2
commit 78a55ab
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
@@ -286,7 +286,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
     -- block reduction immediately under codata (and not forced)
     ev ntimes stk top env
               (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
-       | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl
+       | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)
             = do let (f, _) = unApply arg
                  let ntimes' = case f of
                                     P _ fn _ -> (fn, 0) : ntimes