@@ -12,7 +12,7 @@ module Idris.REPL(
1212 getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc
1313 , getPkgREPL, getPkgTest, getPort, getIBCSubDir
1414 , idris, idrisMain, loadInputs
15− , opt, runClient, runMain, ver
15+ , opt, runClient, runMain
1616 ) where
1717
1818import Idris.AbsSyntax
@@ -55,6 +55,8 @@ import Idris.Elab.Data
5555import Idris.Elab.Value
5656import Idris.Elab.Term
5757
58+import Idris.Info
59+
5860import Version_idris (gitHash)
5961import Util.System
6062import Util.DynamicLinker
@@ -71,7 +73,7 @@ import Idris.Core.Constraints
7173import IRTS.Compiler
7274import IRTS.CodegenCommon
7375import IRTS.Exports
74−import IRTS.System
76+--import IRTS.System
7577
7678import Control.Category
7779import qualified Control.Exception as X
@@ -567,7 +569,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =
567569 msg = (IdeMode.SymbolAtom "ok", out, spans)
568570 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
569571runIdeModeCommand h id orig fn modes IdeMode.GetIdrisVersion =
570− let idrisVersion = (versionBranch version,
572+ let idrisVersion = (versionBranch getIdrisVersionNoGit,
571573 if not (null gitHash)
572574 then [gitHash]
573575 else [])
@@ -1472,7 +1474,7 @@ showTotalN ist n = case lookupTotal n (tt_ctxt ist) of
14721474 showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
14731475 showName (Just ist) [] ppo False n
14741476
1475−displayHelp = let vstr = showVersion version in
1477+displayHelp = let vstr = showVersion getIdrisVersionNoGit in
14761478 "\nIdris version " ++ vstr ++ "\n" ++
14771479 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
14781480 concatMap cmdInfo helphead ++
@@ -1799,13 +1801,13 @@ idrisMain opts =
17991801 Just expr -> execScript expr
18001802
18011803 -- Create Idris data dir + repl history and config dir
1802− idrisCatch (do dir <- getIdrisUserDataDir
1804+ idrisCatch (do dir <- runIO $ getIdrisUserDataDir
18031805 exists <- runIO $ doesDirectoryExist dir
18041806 unless exists $ logLvl 1 ("Creating " ++ dir)
18051807 runIO $ createDirectoryIfMissing True (dir </> "repl"))
18061808 (\e -> return ())
18071809
1808− historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1810+ historyFile <- runIO $ getIdrisHistoryFile
18091811
18101812 when ok $ case opt getPkgIndex opts of
18111813 (f : _) -> writePkgIndex f
@@ -1850,18 +1852,10 @@ execScript expr = do i <- getIState
18501852 res <- execute tm
18511853 runIO $ exitSuccess
18521854
1853−-- | Get the platform-specific, user-specific Idris dir
1854−getIdrisUserDataDir :: Idris FilePath
1855−getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1856−
1857−-- | Locate the platform-specific location for the init script
1858−getInitScript :: Idris FilePath
1859−getInitScript = do idrisDir <- getIdrisUserDataDir
1860− return $ idrisDir </> "repl" </> "init"
18611855
18621856-- | Run the initialisation script
18631857initScript :: Idris ()
1864−initScript = do script <- getInitScript
1858+initScript = do script <- runIO $ getIdrisInitScript
18651859 idrisCatch (do go <- runIO $ doesFileExist script
18661860 when go $ do
18671861 h <- runIO $ openFile script ReadMode
@@ -1873,7 +1867,7 @@ initScript = do script <- getInitScript
18731867 ist <- getIState
18741868 unless eof $ do
18751869 line <- runIO $ hGetLine h
1876− script <- getInitScript
1870+ script <- runIO $ getIdrisInitScript
18771871 c <- colourise
18781872 processLine ist line script c
18791873 runInit h
@@ -2011,16 +2005,17 @@ getPort (_:xs) = getPort xs
20112005opt :: (Opt -> Maybe a) -> [Opt] -> [a]
20122006opt = mapMaybe
20132007
2008+{-
20142009ver = showVersion version ++ suffix
20152010 where
20162011 suffix = if gitHash =="" then "" else "-" ++ gitHash
2017−
2012+-}
20182013defaultPort :: PortID
20192014defaultPort = PortNumber (fromIntegral 4294)
20202015
20212016banner = " ____ __ _ \n" ++
20222017 " / _/___/ /____(_)____ \n" ++
2023− " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
2018+ " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
20242019 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
20252020 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
20262021 "\n" ++