git.iko.soy/Idris-dev
on master help sign in
Have the REPL save its history between sessions
da87313David Christiansen
src/Idris/REPL.hs+15−6
compare with master
unifiedsplit
@@ -655,8 +655,10 @@ helphead =
655 ]
655 ]
656
656
657
657
658−replSettings :: Settings Idris
658+replSettings :: Maybe FilePath -> Settings Idris
659−replSettings = setComplete replCompletion defaultSettings
659+replSettings hFile = setComplete replCompletion $ defaultSettings {
660+ historyFile = hFile
661+ }
660
662
661-- invoke as if from command line
663-- invoke as if from command line
662idris :: [Opt] -> IO IState
664idris :: [Opt] -> IO IState
@@ -725,7 +727,7 @@ loadInputs inputs
725
727
726 ibc (IBC _ _) = True
728 ibc (IBC _ _) = True
727 ibc _ = False
729 ibc _ = False
728−
730+
729idrisMain :: [Opt] -> Idris ()
731idrisMain :: [Opt] -> Idris ()
730idrisMain opts =
732idrisMain opts =
731 do let inputs = opt getFile opts
733 do let inputs = opt getFile opts
@@ -806,8 +808,11 @@ idrisMain opts =
806 case script of
808 case script of
807 Nothing -> return ()
809 Nothing -> return ()
808 Just expr -> execScript expr
810 Just expr -> execScript expr
811+
812+ historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
813+
809 when runrepl $ initScript
814 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
811 when (idesl) $ ideslaveStart ist inputs
816 when (idesl) $ ideslaveStart ist inputs
812 ok <- noErrors
817 ok <- noErrors
813 when (not ok) $ liftIO (exitWith (ExitFailure 1))
818 when (not ok) $ liftIO (exitWith (ExitFailure 1))
@@ -820,7 +825,7 @@ idrisMain opts =
820 makeOption _ = return ()
825 makeOption _ = return ()
821
826
822 addPkgDir :: String -> Idris ()
827 addPkgDir :: String -> Idris ()
823− addPkgDir p = do ddir <- liftIO $ getDataDir
828+ addPkgDir p = do ddir <- liftIO $ getDataDir
824 addImportDir (ddir </> p)
829 addImportDir (ddir </> p)
825
830
826execScript :: String -> Idris ()
831execScript :: String -> Idris ()
@@ -833,9 +838,13 @@ execScript expr = do i <- getIState
833 res <- execute tm
838 res <- execute tm
834 liftIO $ exitWith ExitSuccess
839 liftIO $ exitWith ExitSuccess
835
840
841+-- | Get the platform-specific, user-specific Idris dir
842+getIdrisUserDataDir :: Idris FilePath
843+getIdrisUserDataDir = liftIO $ getAppUserDataDirectory "idris"
844+
836-- | Locate the platform-specific location for the init script
845-- | Locate the platform-specific location for the init script
837getInitScript :: Idris FilePath
846getInitScript :: Idris FilePath
838−getInitScript = do idrisDir <- lift $ getAppUserDataDirectory "idris"
847+getInitScript = do idrisDir <- getIdrisUserDataDir
839 return $ idrisDir </> "repl" </> "init"
848 return $ idrisDir </> "repl" </> "init"
840
849
841-- | Run the initialisation script
850-- | Run the initialisation script