@@ -113,7 +113,7 @@ ideslave orig mods
113113 do let fn = case mods of
114114 (f:_) -> f
115115 _ -> ""
116− case parseCmd i cmd of
116+ case parseCmd i "(input)" cmd of
117117 Left err -> iFail $ show err
118118 Right (Prove n') -> do iResult ""
119119 idrisCatch
@@ -214,7 +214,7 @@ processInput cmd orig inputs
214214 let fn = case inputs of
215215 (f:_) -> f
216216 _ -> ""
217− case parseCmd i cmd of
217+ case parseCmd i "(input)" cmd of
218218 Left err -> do liftIO $ print err
219219 return (Just inputs)
220220 Right Reload ->
@@ -794,7 +794,7 @@ idrisMain opts =
794794 return ()
795795 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
796796 ist <- getIState
797−
797+
798798 loadInputs inputs
799799
800800 liftIO $ hSetBuffering stdout LineBuffering
@@ -806,6 +806,7 @@ idrisMain opts =
806806 case script of
807807 Nothing -> return ()
808808 Just expr -> execScript expr
809+ when runrepl $ initScript
809810 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
810811 when (idesl) $ ideslaveStart ist inputs
811812 ok <- noErrors
@@ -832,6 +833,39 @@ execScript expr = do i <- getIState
832833 res <- execute tm
833834 liftIO $ exitWith ExitSuccess
834835
836+-- | Locate the platform-specific location for the init script
837+getInitScript :: Idris FilePath
838+getInitScript = do idrisDir <- lift $ getAppUserDataDirectory "idris"
839+ return $ idrisDir </> "repl" </> "init"
840+
841+-- | Run the initialisation script
842+initScript :: Idris ()
843+initScript = do script <- getInitScript
844+ idrisCatch (do go <- liftIO $ doesFileExist script
845+ when go $ do
846+ h <- liftIO $ openFile script ReadMode
847+ runInit h
848+ liftIO $ hClose h)
849+ (\e -> iFail $ "Error reading init file: " ++ show e)
850+ where runInit :: Handle -> Idris ()
851+ runInit h = do eof <- lift (hIsEOF h)
852+ ist <- getIState
853+ unless eof $ do
854+ line <- liftIO $ hGetLine h
855+ script <- getInitScript
856+ processLine ist line script
857+ runInit h
858+ processLine i cmd input =
859+ case parseCmd i input cmd of
860+ Left err -> liftIO $ print err
861+ Right Reload -> iFail "Init scripts cannot reload the file"
862+ Right (Load f) -> iFail "Init scripts cannot load files"
863+ Right (ModImport f) -> iFail "Init scripts cannot import modules"
864+ Right Edit -> iFail "Init scripts cannot invoke the editor"
865+ Right Proofs -> proofs i
866+ Right Quit -> iFail "Init scripts cannot quit Idris"
867+ Right cmd -> process [] cmd
868+
835869getFile :: Opt -> Maybe String
836870getFile (Filename str) = Just str
837871getFile _ = Nothing