git.iko.soy/Idris-dev
on master help sign in
"it" now refers to the previous value at the REPL
506d367Edwin Brady
CHANGELOG+5
compare with master
unifiedsplit
@@ -1,3 +1,8 @@
1+New in 0.9.10:
2+--------------
3+
4+* At the REPL, "it" now refers to the previous expression
5+
1New in 0.9.9:
6New in 0.9.9:
2-------------
7-------------
3
8
src/Idris/REPL.hs+2
@@ -300,6 +300,8 @@ process fn (Eval t)
300 ist <- getIState
300 ist <- getIState
301 let tm' = normaliseAll ctxt [] tm
301 let tm' = normaliseAll ctxt [] tm
302 let ty' = normaliseAll ctxt [] ty
302 let ty' = normaliseAll ctxt [] ty
303+ -- Add value to context, call it "it"
304+ updateContext (addCtxtDef (UN "it") (Function ty' tm'))
303 logLvl 3 $ "Raw: " ++ show (tm', ty')
305 logLvl 3 $ "Raw: " ++ show (tm', ty')
304 imp <- impShow
306 imp <- impShow
305 iResult (showImp imp (delab ist tm') ++ " : " ++
307 iResult (showImp imp (delab ist tm') ++ " : " ++