8125e03 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add support for init scripts

8125e03David Christiansen13 years ago

src/Idris/REPL.hs+37−3

compare with master

unifiedsplit

@@ -113,7 +113,7 @@ ideslave orig mods

113 do let fn = case mods of

114 (f:_) -> f

115 _ -> ""

116− case parseCmd i cmd of

116+ case parseCmd i "(input)" cmd of

117 Left err -> iFail $ show err

118 Right (Prove n') -> do iResult ""

119 idrisCatch

@@ -214,7 +214,7 @@ processInput cmd orig inputs

214 let fn = case inputs of

215 (f:_) -> f

216 _ -> ""

217− case parseCmd i cmd of

217+ case parseCmd i "(input)" cmd of

218 Left err -> do liftIO $ print err

219 return (Just inputs)

220 Right Reload ->

@@ -794,7 +794,7 @@ idrisMain opts =

794 return ()

795 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner

796 ist <- getIState

797−

797+

798 loadInputs inputs

799

800 liftIO $ hSetBuffering stdout LineBuffering

@@ -806,6 +806,7 @@ idrisMain opts =

806 case script of

807 Nothing -> return ()

808 Just expr -> execScript expr

809+ when runrepl $ initScript

809 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs

810 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs

810 when (idesl) $ ideslaveStart ist inputs

811 when (idesl) $ ideslaveStart ist inputs

811 ok <- noErrors

812 ok <- noErrors

@@ -832,6 +833,39 @@ execScript expr = do i <- getIState

832 res <- execute tm

833 res <- execute tm

833 liftIO $ exitWith ExitSuccess

834 liftIO $ exitWith ExitSuccess

834

835

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+

835getFile :: Opt -> Maybe String

869getFile :: Opt -> Maybe String

836getFile (Filename str) = Just str

870getFile (Filename str) = Just str

837getFile _ = Nothing

871getFile _ = Nothing

src/Idris/REPLParser.hs+2−1

@@ -18,7 +18,8 @@ import Data.List

18import Data.List.Split(splitOn)

19import Data.Char(toLower)

21+parseCmd :: IState -> String -> String -> Either ParseError Command

21−parseCmd i = runParser pCmd i "(input)"

22+parseCmd i inputname = runParser pCmd i inputname

23cmd :: [String] -> IParser ()

24cmd :: [String] -> IParser ()

24cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

25cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)