4fd6bc6 · Idris-dev · git.iko.soy

main/Main.hs+5−3

compare with master

unifiedsplit

@@ -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

@@ -201,9 +199,9 @@ processNetCmd orig i h fn cmd

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

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

202

200

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

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

204−runClient :: String -> IO ()

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

205−runClient str = withSocketsDo $ do

203+runClient port str = withSocketsDo $ do

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

204+ h <- connectTo "localhost" port

207 hSetEncoding h utf8

205 hSetEncoding h utf8

208 hPutStrLn h str

206 hPutStrLn h str

209 resp <- hGetResp "" h

207 resp <- hGetResp "" h

@@ -1428,6 +1426,7 @@ idrisMain opts =

1428 runIO $ exitWith (ExitFailure 1)

1426 runIO $ exitWith (ExitFailure 1)

1429 [expr] -> return (Just expr)

1427 [expr] -> return (Just expr)

1430 let immediate = opt getEvalExpr opts

1428 let immediate = opt getEvalExpr opts

1429+ let port = getPort opts

1431

1430

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

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

1433 putIState (i { default_total = True })

1432 putIState (i { default_total = True })

@@ -1516,7 +1515,7 @@ idrisMain opts =

1516

1515

1517 when (runrepl && not idesl) $ do

1516 when (runrepl && not idesl) $ do

1518-- clearOrigPats

1517-- clearOrigPats

1519− startServer orig inputs

1518+ startServer port orig inputs

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

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

1521 let idesock = IdeslaveSocket `elem` opts

1520 let idesock = IdeslaveSocket `elem` opts

1522 when (idesl) $ ideslaveStart idesock orig inputs

1521 when (idesl) $ ideslaveStart idesock orig inputs

@@ -1679,11 +1678,26 @@ getColour :: Opt -> Maybe Bool

1679getColour (ColourREPL b) = Just b

1678getColour (ColourREPL b) = Just b

1680getColour _ = Nothing

1679getColour _ = Nothing

1681

1680

1681+getClient :: Opt -> Maybe String

1682+getClient (Client x) = Just x

1683+getClient _ = Nothing

1684+

1685+-- Get the first valid port

1686+getPort :: [Opt] -> PortID

1687+getPort [] = defaultPort

1688+getPort (Port p:xs)

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

1690+ | otherwise = getPort xs

1691+getPort (_:xs) = getPort xs

1692+

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

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

1683opt = mapMaybe

1694opt = mapMaybe

1684

1695

1685ver = showVersion version ++ gitHash

1696ver = showVersion version ++ gitHash

1686

1697

1698+defaultPort :: PortID

1699+defaultPort = PortNumber (fromIntegral 4294)

1700+

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

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

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

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

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

1703 " / // __ / ___/ / ___/ 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