840c2cc · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -409,6 +409,10 @@ Extra-source-files:

409 test/interactive005/input

410 test/interactive005/*.idr

411 test/interactive005/expected

412+ test/interactive006/run

413+ test/interactive006/input

414+ test/interactive006/*.idr

415+ test/interactive006/expected

412

416

413 test/io001/run

417 test/io001/run

414 test/io001/*.idr

418 test/io001/*.idr

main/Main.hs+5−3

@@ -42,13 +42,15 @@ main = do opts <- runArgParser

42 runMain (runIdris opts)

43

44runIdris :: [Opt] -> Idris ()

45−runIdris [Client c] = do setVerbose False

46− setQuiet True

47− runIO $ runClient c

48runIdris opts = do

45runIdris opts = do

49 when (ShowIncs `elem` opts) $ runIO showIncs

46 when (ShowIncs `elem` opts) $ runIO showIncs

50 when (ShowLibs `elem` opts) $ runIO showLibs

47 when (ShowLibs `elem` opts) $ runIO showLibs

51 when (ShowLibdir `elem` opts) $ runIO showLibdir

48 when (ShowLibdir `elem` opts) $ runIO showLibdir

49+ case opt getClient opts of

50+ [] -> return ()

51+ (c:_) -> do setVerbose False

52+ setQuiet True

53+ runIO $ runClient (getPort opts) c

52 case opt getPkgCheck opts of

54 case opt getPkgCheck opts of

53 [] -> return ()

55 [] -> return ()

54 fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs

56 fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs

src/Idris/AbsSyntaxTree.hs+1

@@ -393,6 +393,7 @@ data Opt = Filename String

393 | ErrContext

394 | ShowImpl

395 | Verbose

396+ | Port String -- REPL TCP port

396 | IBCSubDir String

397 | IBCSubDir String

397 | ImportDir String

398 | ImportDir String

398 | PkgBuild String

399 | PkgBuild String

src/Idris/CmdOptions.hs+1

@@ -96,6 +96,7 @@ parseFlags = many $

96 <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

97 <|> flag' WarnOnly (long "warn")

98 <|> (Pkg <$> strOption (short 'p' <> long "package"))

99+ <|> (Port <$> strOption (long "port" <> metavar "PORT" <> help "REPL TCP port"))

99 -- Package commands

100 -- Package commands

100 <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

101 <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

101 <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

102 <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

src/Idris/REPL.hs+26−12

@@ -140,14 +140,12 @@ repl orig mods

140 showM c thm n = if c then colouriseFun thm (show n)

141 else show n

142

143−-- | Run the REPL server

143+-- | Run the REPL seDver

144−startServer :: IState -> [FilePath] -> Idris ()

144+startServer :: PortID -> IState -> [FilePath] -> Idris ()

145−startServer orig fn_in = do tid <- runIO $ forkOS serverLoop

145+startServer port orig fn_in = do tid <- runIO $ forkOS (serverLoop port)

146− return ()

146+ return ()

147− where serverLoop :: IO ()

147+ where serverLoop port = withSocketsDo $

148− -- TODO: option for port number

149− serverLoop = withSocketsDo $

150− do sock <- listenOnLocalhost $ PortNumber 4294

148+ do sock <- listenOnLocalhost port

151 loop fn orig { idris_colourRepl = False } sock

149 loop fn orig { idris_colourRepl = False } sock

152

150

153 fn = case fn_in of

151 fn = case fn_in of

@@ -202,9 +200,9 @@ processNetCmd orig i h fn cmd

202 IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

200 IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

203

201

204-- | Run a command on the server on localhost

202-- | Run a command on the server on localhost

205−runClient :: String -> IO ()

203+runClient :: PortID -> String -> IO ()

206−runClient str = withSocketsDo $ do

204+runClient port str = withSocketsDo $ do

207− h <- connectTo "localhost" (PortNumber 4294)

205+ h <- connectTo "localhost" port

208 hSetEncoding h utf8

206 hSetEncoding h utf8

209 hPutStrLn h str

207 hPutStrLn h str

210 resp <- hGetResp "" h

208 resp <- hGetResp "" h

@@ -1431,6 +1429,7 @@ idrisMain opts =

1431 runIO $ exitWith (ExitFailure 1)

1429 runIO $ exitWith (ExitFailure 1)

1432 [expr] -> return (Just expr)

1430 [expr] -> return (Just expr)

1433 let immediate = opt getEvalExpr opts

1431 let immediate = opt getEvalExpr opts

1432+ let port = getPort opts

1434

1433

1435 when (DefaultTotal `elem` opts) $ do i <- getIState

1434 when (DefaultTotal `elem` opts) $ do i <- getIState

1436 putIState (i { default_total = True })

1435 putIState (i { default_total = True })

@@ -1519,7 +1518,7 @@ idrisMain opts =

1519

1518

1520 when (runrepl && not idesl) $ do

1519 when (runrepl && not idesl) $ do

1521-- clearOrigPats

1520-- clearOrigPats

1522− startServer orig inputs

1521+ startServer port orig inputs

1523 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1522 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1524 let idesock = IdeslaveSocket `elem` opts

1523 let idesock = IdeslaveSocket `elem` opts

1525 when (idesl) $ ideslaveStart idesock orig inputs

1524 when (idesl) $ ideslaveStart idesock orig inputs

@@ -1683,11 +1682,26 @@ getColour :: Opt -> Maybe Bool

1683getColour (ColourREPL b) = Just b

1682getColour (ColourREPL b) = Just b

1684getColour _ = Nothing

1683getColour _ = Nothing

1685

1684

1685+getClient :: Opt -> Maybe String

1686+getClient (Client x) = Just x

1687+getClient _ = Nothing

1688+

1689+-- Get the first valid port

1690+getPort :: [Opt] -> PortID

1691+getPort [] = defaultPort

1692+getPort (Port p:xs)

1693+ | all (`elem` ['0'..'9']) p = PortNumber $ fromIntegral (read p)

1694+ | otherwise = getPort xs

1695+getPort (_:xs) = getPort xs

1696+

1686opt :: (Opt -> Maybe a) -> [Opt] -> [a]

1697opt :: (Opt -> Maybe a) -> [Opt] -> [a]

1687opt = mapMaybe

1698opt = mapMaybe

1688

1699

1689ver = showVersion version ++ gitHash

1700ver = showVersion version ++ gitHash

1690

1701

1702+defaultPort :: PortID

1703+defaultPort = PortNumber (fromIntegral 4294)

1704+

1691banner = " ____ __ _ \n" ++

1705banner = " ____ __ _ \n" ++

1692 " / _/___/ /____(_)____ \n" ++

1706 " / _/___/ /____(_)____ \n" ++

1693 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1707 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

test/interactive006/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./interactive006.idr

2+plus ?foo_rhs2 ?foo_rhs3

test/interactive006/inputnew file+1

@@ -0,0 +1 @@

1+:ref 2 foo_rhs1 plus

test/interactive006/interactive006.idrnew file+3

@@ -0,0 +1,3 @@

1+foo : Nat -> Nat -> Nat

2+foo k j = ?foo_rhs1

3+

test/interactive006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet --port 5000 interactive006.idr < input

3+rm -f *.ibc