@@ -180,6 +180,7 @@ receiveInput e =
180180 ideslavePutSExp "return" good
181181 receiveInput e
182182 Just (Interpret cmd) -> return (Just cmd)
183+ Just (TypeOf str) -> return (Just (":t " ++ str))
183184 _ -> return Nothing
184185
185186ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
@@ -211,21 +212,21 @@ ploop fn d prompt prf e h
211212 (case cmd of
212213 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
213214 Success Undo -> do (_, st) <- elabStep e loadState
214− return (True, st, False, init prf, Right "")
215− Success ProofState -> return (True, e, False, prf, Right "")
215+ return (True, st, False, init prf, Right $ iPrintResult "")
216+ Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
216217 Success ProofTerm -> do tm <- lifte e get_term
217218 iputStrLn $ "TT: " ++ show tm ++ "\n"
218− return (False, e, False, prf, Right "")
219+ return (False, e, False, prf, Right $ iPrintResult "")
219220 Success Qed -> do hs <- lifte e get_holes
220221 when (not (null hs)) $ ifail "Incomplete proof"
221222 iputStrLn "Proof completed!"
222− return (False, e, True, prf, Right "")
223+ return (False, e, True, prf, Right $ iPrintResult "")
223224 Success (TCheck (PRef _ n)) -> checkNameType n
224225 Success (TCheck t) -> checkType t
225226 Success (TEval t) -> evalTerm t e
226227 Success tac -> do (_, e) <- elabStep e saveState
227228 (_, st) <- elabStep e (runTac autoSolve i fn tac)
228− return (True, st, False, prf ++ [step], Right ""))
229+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
229230 (\err -> return (False, e, False, prf, Left err))
230231 ideslavePutSExp "write-proof-state" (prf', length prf')
231232 case res of
@@ -234,7 +235,7 @@ ploop fn d prompt prf e h
234235 Right ok ->
235236 if done then do (tm, _) <- elabStep st get_term
236237 return (tm, prf')
237− else do iPrintResult ok
238+ else do ok
238239 ploop fn d prompt prf' st h'
239240 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
240241 checkNameType n = do
@@ -250,11 +251,11 @@ ploop fn d prompt prf e h
250251 putIState ist'
251252 -- Unlike the REPL, metavars have no special treatment, to
252253 -- make it easier to see how to prove with them.
253− case lookupNames n ctxt' of
254− [] -> ihPrintError h $ "No such variable " ++ show n
255− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
254+ let action = case lookupNames n ctxt' of
255+ [] -> ihPrintError h $ "No such variable " ++ show n
256+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
256257 putIState ist
257− return (False, e, False, prf, Right ""))
258+ return (False, e, False, prf, Right action))
258259 (\err -> do putIState ist ; ierror err)
259260
260261 checkType t = do
@@ -269,14 +270,14 @@ ploop fn d prompt prf e h
269270 ty' = normaliseC ctxt [] ty
270271 h = idris_outh ist
271272 infixes = idris_infixes ist
272− case tm of
273− TType _ ->
274− ihPrintTermWithType h (prettyImp ppo PType) type1Doc
275− _ -> let bnd = map (\x -> (fst x, False)) env in
276− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
277− (pprintPTerm ppo bnd [] infixes (delab ist ty))
273+ action = case tm of
274+ TType _ ->
275+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
276+ _ -> let bnd = map (\x -> (fst x, False)) env in
277+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
278+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
278279 putIState ist
279− return (False, e, False, prf, Right ""))
280+ return (False, e, False, prf, Right action))
280281 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
281282
282283 evalTerm t e = withErrorReflection $
@@ -295,7 +296,7 @@ ploop fn d prompt prf e h
295296 infixes = idris_infixes ist
296297 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
297298 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
298− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
299+ action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
299300 putIState ist
300− return (False, e, False, prf, Right ""))
301+ return (False, e, False, prf, Right action))
301302 (\err -> do putIState ist ; ierror err)