@@ -263,6 +263,13 @@ execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
263 "The argument to idris_readStr should be a handle, but it was " ++
263 "The argument to idris_readStr should be a handle, but it was " ++
264 show handle ++
264 show handle ++
265 ". Are all cases covered?"
265 ". Are all cases covered?"
266+execApp env ctxt (EP _ fp _) (_:fn:_:rest)
268+ Just (FFun "getchar" _ _) <- foreignFromTT fn
269+ = do -- The C API returns an Int which Idris library code
270+ -- converts; thus, we must make an int here.
271+ ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar
272+ execApp env ctxt ch rest
266execApp env ctxt (EP _ fp _) (_:fn:rest)
273execApp env ctxt (EP _ fp _) (_:fn:rest)
267 | fp == mkfprim,
274 | fp == mkfprim,
268 Just (FFun "idris_time" _ _) <- foreignFromTT fn
275 Just (FFun "idris_time" _ _) <- foreignFromTT fn