@@ -16,6 +16,7 @@ import Idris.DataOpts
1616import Idris.Completion
1717
1818import System.Console.Haskeline
19+import System.Console.Haskeline.History
1920import Control.Monad.State
2021
2122import Util.Pretty
@@ -49,7 +50,7 @@ proverSettings e = setComplete (proverCompletion assumptionNames) defaultSetting
4950prove :: Context -> Bool -> Name -> Type -> Idris ()
5051prove ctxt lit n ty
5152 = do let ps = initElaborator n ctxt ty
52− (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)
53+ (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
5354 iLOG $ "Adding " ++ show tm
5455 iputStrLn $ showProof lit n prf
5556 i <- getIState
@@ -117,11 +118,18 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
117118lifte st e = do (v, _) <- elabStep st e
118119 return v
119120
120−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])
121−ploop d prompt prf e
121+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
122+ploop d prompt prf e h
122123 = do i <- getIState
123124 when d $ liftIO $ dumpState i (proof e)
124− x <- runInputT (proverSettings e) $ getInputLine (prompt ++ "> ")
125+ (x, h') <- runInputT (proverSettings e) $
126+ -- Manually track the history so that we can use the proof state
127+ do _ <- case h of
128+ Just history -> putHistory history
129+ Nothing -> return ()
130+ l <- getInputLine (prompt ++ "> ")
131+ h' <- getHistory
132+ return (l, Just h')
125133 (cmd, step) <- case x of
126134 Nothing -> fail "Abandoned"
127135 Just input -> do return (parseTac i input, input)
@@ -151,5 +159,5 @@ ploop d prompt prf e
151159 return (False, e, False, prf))
152160 if done then do (tm, _) <- elabStep st get_term
153161 return (tm, prf')
154− else ploop d prompt prf' st
162+ else ploop d prompt prf' st h'
155163