@@ -655,8 +655,10 @@ helphead =
655655 ]
656656
657657
658−replSettings :: Settings Idris
659−replSettings = setComplete replCompletion defaultSettings
658+replSettings :: Maybe FilePath -> Settings Idris
659+replSettings hFile = setComplete replCompletion $ defaultSettings {
660+ historyFile = hFile
661+ }
660662
661663-- invoke as if from command line
662664idris :: [Opt] -> IO IState
@@ -725,7 +727,7 @@ loadInputs inputs
725727
726728 ibc (IBC _ _) = True
727729 ibc _ = False
728−
730+
729731idrisMain :: [Opt] -> Idris ()
730732idrisMain opts =
731733 do let inputs = opt getFile opts
@@ -806,8 +808,11 @@ idrisMain opts =
806808 case script of
807809 Nothing -> return ()
808810 Just expr -> execScript expr
811+
812+ historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
813+
809814 when runrepl $ initScript
810− when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
815+ when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs
811816 when (idesl) $ ideslaveStart ist inputs
812817 ok <- noErrors
813818 when (not ok) $ liftIO (exitWith (ExitFailure 1))
@@ -820,7 +825,7 @@ idrisMain opts =
820825 makeOption _ = return ()
821826
822827 addPkgDir :: String -> Idris ()
823− addPkgDir p = do ddir <- liftIO $ getDataDir
828+ addPkgDir p = do ddir <- liftIO $ getDataDir
824829 addImportDir (ddir </> p)
825830
826831execScript :: String -> Idris ()
@@ -833,9 +838,13 @@ execScript expr = do i <- getIState
833838 res <- execute tm
834839 liftIO $ exitWith ExitSuccess
835840
841+-- | Get the platform-specific, user-specific Idris dir
842+getIdrisUserDataDir :: Idris FilePath
843+getIdrisUserDataDir = liftIO $ getAppUserDataDirectory "idris"
844+
836845-- | Locate the platform-specific location for the init script
837846getInitScript :: Idris FilePath
838−getInitScript = do idrisDir <- lift $ getAppUserDataDirectory "idris"
847+getInitScript = do idrisDir <- getIdrisUserDataDir
839848 return $ idrisDir </> "repl" </> "init"
840849
841850-- | Run the initialisation script