@@ -9,6 +9,7 @@ import Idris.Core.Typecheck
99import Idris.AbsSyntax
1010import Idris.AbsSyntaxTree
1111import Idris.Delaborate
12+import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
1213import Idris.ElabDecls
1314import Idris.ElabTerm
1415import Idris.Parser hiding (params)
@@ -180,6 +181,8 @@ receiveInput e =
180181 ideslavePutSExp "return" good
181182 receiveInput e
182183 Just (Interpret cmd) -> return (Just cmd)
184+ Just (TypeOf str) -> return (Just (":t " ++ str))
185+ Just (DocsFor str) -> return (Just (":doc " ++ str))
183186 _ -> return Nothing
184187
185188ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
@@ -211,21 +214,22 @@ ploop fn d prompt prf e h
211214 (case cmd of
212215 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
213216 Success Undo -> do (_, st) <- elabStep e loadState
214− return (True, st, False, init prf, Right "")
215− Success ProofState -> return (True, e, False, prf, Right "")
217+ return (True, st, False, init prf, Right $ iPrintResult "")
218+ Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
216219 Success ProofTerm -> do tm <- lifte e get_term
217220 iputStrLn $ "TT: " ++ show tm ++ "\n"
218− return (False, e, False, prf, Right "")
221+ return (False, e, False, prf, Right $ iPrintResult "")
219222 Success Qed -> do hs <- lifte e get_holes
220223 when (not (null hs)) $ ifail "Incomplete proof"
221224 iputStrLn "Proof completed!"
222− return (False, e, True, prf, Right "")
225+ return (False, e, True, prf, Right $ iPrintResult "")
223226 Success (TCheck (PRef _ n)) -> checkNameType n
224227 Success (TCheck t) -> checkType t
225228 Success (TEval t) -> evalTerm t e
229+ Success (TDocStr x) -> docStr x
226230 Success tac -> do (_, e) <- elabStep e saveState
227231 (_, st) <- elabStep e (runTac autoSolve i fn tac)
228− return (True, st, False, prf ++ [step], Right ""))
232+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
229233 (\err -> return (False, e, False, prf, Left err))
230234 ideslavePutSExp "write-proof-state" (prf', length prf')
231235 case res of
@@ -234,7 +238,7 @@ ploop fn d prompt prf e h
234238 Right ok ->
235239 if done then do (tm, _) <- elabStep st get_term
236240 return (tm, prf')
237− else do iPrintResult ok
241+ else do ok
238242 ploop fn d prompt prf' st h'
239243 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
240244 checkNameType n = do
@@ -250,11 +254,11 @@ ploop fn d prompt prf e h
250254 putIState ist'
251255 -- Unlike the REPL, metavars have no special treatment, to
252256 -- 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)
257+ let action = case lookupNames n ctxt' of
258+ [] -> ihPrintError h $ "No such variable " ++ show n
259+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
256260 putIState ist
257− return (False, e, False, prf, Right ""))
261+ return (False, e, False, prf, Right action))
258262 (\err -> do putIState ist ; ierror err)
259263
260264 checkType t = do
@@ -269,14 +273,14 @@ ploop fn d prompt prf e h
269273 ty' = normaliseC ctxt [] ty
270274 h = idris_outh ist
271275 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))
276+ action = case tm of
277+ TType _ ->
278+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
279+ _ -> let bnd = map (\x -> (fst x, False)) env in
280+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
281+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
278282 putIState ist
279− return (False, e, False, prf, Right ""))
283+ return (False, e, False, prf, Right action))
280284 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
281285
282286 evalTerm t e = withErrorReflection $
@@ -295,7 +299,22 @@ ploop fn d prompt prf e h
295299 infixes = idris_infixes ist
296300 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
297301 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
298− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
302+ action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
299303 putIState ist
300− return (False, e, False, prf, Right ""))
304+ return (False, e, False, prf, Right action))
301305 (\err -> do putIState ist ; ierror err)
306+ docStr :: Either Name Const -> Idris (Bool, ElabState [PDecl], Bool, [String], Either Err (Idris ()))
307+ docStr (Left n) = do ist <- getIState
308+ let h = idris_outh ist
309+ idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
310+ [] -> return (False, e, False, prf,
311+ Left . Msg $ "No documentation for " ++ show n)
312+ ns -> do toShow <- mapM (showDoc ist) ns
313+ return (False, e, False, prf,
314+ Right $ ihRenderResult h (vsep toShow)))
315+ (\err -> do putIState ist ; ierror err)
316+ where showDoc ist (n, d) = do doc <- getDocs n
317+ return $ pprintDocs ist doc
318+ docStr (Right c) = do ist <- getIState
319+ let h = idris_outh ist
320+ return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))