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

git.iko.soy/Idris-dev

Merge pull request #1556 from Helkafen/master

Allow REPL to run on another port (flag --port)

commit840c2cc629fcec5fbbf011ad08398f66e368bddf authorDavid Christiansen <david@davidchristiansen.dk> dateTue 30 Sep 2014, 17:53 (12 years ago) parentd5c5e30 f10fcd2

9 files changed+46−15

compare with master

unifiedsplit

idris.cabal+4 main/Main.hs+5−3 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CmdOptions.hs+1 src/Idris/REPL.hs+26−12 test/interactive006/expected+2 test/interactive006/input+1 test/interactive006/interactive006.idr+3 test/interactive006/run+3

idris.cabal+4

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

409409 test/interactive005/input

410410 test/interactive005/*.idr

411411 test/interactive005/expected

412+ test/interactive006/run

413+ test/interactive006/input

414+ test/interactive006/*.idr

415+ test/interactive006/expected

412416

413417 test/io001/run

414418 test/io001/*.idr

main/Main.hs+5−3

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

4242 runMain (runIdris opts)

4343

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

45−runIdris [Client c] = do setVerbose False

46− setQuiet True

47− runIO $ runClient c

4845runIdris opts = do

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

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

5148 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

5254 case opt getPkgCheck opts of

5355 [] -> return ()

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

src/Idris/AbsSyntaxTree.hs+1

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

393393 | ErrContext

394394 | ShowImpl

395395 | Verbose

396+ | Port String -- REPL TCP port

396397 | IBCSubDir String

397398 | ImportDir String

398399 | PkgBuild String

src/Idris/CmdOptions.hs+1

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

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

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

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

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

99100 -- Package commands

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

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

src/Idris/REPL.hs+26−12

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

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

141141 else show n

142142

143−-- | Run the REPL server

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

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

146− return ()

147− where serverLoop :: IO ()

148− -- TODO: option for port number

149− serverLoop = withSocketsDo $

150− do sock <- listenOnLocalhost $ PortNumber 4294

143+-- | Run the REPL seDver

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

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

146+ return ()

147+ where serverLoop port = withSocketsDo $

148+ do sock <- listenOnLocalhost port

151149 loop fn orig { idris_colourRepl = False } sock

152150

153151 fn = case fn_in of

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

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

203201

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

205−runClient :: String -> IO ()

206−runClient str = withSocketsDo $ do

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

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

204+runClient port str = withSocketsDo $ do

205+ h <- connectTo "localhost" port

208206 hSetEncoding h utf8

209207 hPutStrLn h str

210208 resp <- hGetResp "" h

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

14311429 runIO $ exitWith (ExitFailure 1)

14321430 [expr] -> return (Just expr)

14331431 let immediate = opt getEvalExpr opts

1432+ let port = getPort opts

14341433

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

14361435 putIState (i { default_total = True })

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

15191518

15201519 when (runrepl && not idesl) $ do

15211520-- clearOrigPats

1522− startServer orig inputs

1521+ startServer port orig inputs

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

15241523 let idesock = IdeslaveSocket `elem` opts

15251524 when (idesl) $ ideslaveStart idesock orig inputs

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

16831682getColour (ColourREPL b) = Just b

16841683getColour _ = Nothing

16851684

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+

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

16871698opt = mapMaybe

16881699

16891700ver = showVersion version ++ gitHash

16901701

1702+defaultPort :: PortID

1703+defaultPort = PortNumber (fromIntegral 4294)

1704+

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

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

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

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