git.iko.soy/Idris-dev
on master help sign in
Remove MVar from REPL
ef0b6ecEdwin Brady
src/Idris/REPL.hs+15−22
compare with master
unifiedsplit
@@ -77,14 +77,12 @@ import Debug.Trace
77
77
78-- | Run the REPL
78-- | Run the REPL
79repl :: IState -- ^ The initial state
79repl :: IState -- ^ The initial state
80− -> MVar IState -- ^ Server's MVar
81 -> [FilePath] -- ^ The loaded modules
80 -> [FilePath] -- ^ The loaded modules
82 -> InputT Idris ()
81 -> InputT Idris ()
83−repl orig stvar mods
82+repl orig mods
84 = H.catch
83 = H.catch
85 (do let quiet = opt_quiet (idris_options orig)
84 (do let quiet = opt_quiet (idris_options orig)
86 i <- lift getIState
85 i <- lift getIState
87− lift $ runIO $ swapMVar stvar i -- update shared state
88 let colour = idris_colourRepl i
86 let colour = idris_colourRepl i
89 let theme = idris_colourTheme i
87 let theme = idris_colourTheme i
90 let mvs = idris_metavars i
88 let mvs = idris_metavars i
@@ -98,15 +96,15 @@ repl orig stvar mods
98 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
96 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
99 return ()
97 return ()
100 Just input -> H.catch
98 Just input -> H.catch
101− (do ms <- lift $ processInput stvar input orig mods
99+ (do ms <- lift $ processInput input orig mods
102 case ms of
100 case ms of
103− Just mods -> repl orig stvar mods
101+ Just mods -> repl orig mods
104 Nothing -> return ())
102 Nothing -> return ())
105 ctrlC)
103 ctrlC)
106 ctrlC
104 ctrlC
107 where ctrlC :: SomeException -> InputT Idris ()
105 where ctrlC :: SomeException -> InputT Idris ()
108 ctrlC e = do lift $ iputStrLn (show e)
106 ctrlC e = do lift $ iputStrLn (show e)
109− repl orig stvar mods
107+ repl orig mods
110
108
111 showMVs c thm [] = ""
109 showMVs c thm [] = ""
112 showMVs c thm ms = "Metavariables: " ++
110 showMVs c thm ms = "Metavariables: " ++
@@ -124,15 +122,14 @@ repl orig stvar mods
124 else show n
122 else show n
125
123
126-- | Run the REPL server
124-- | Run the REPL server
127−startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
125+startServer :: IState -> [FilePath] -> Idris ()
128−startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
126+startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
129− return ()
127+ return ()
130 where serverLoop :: IO ()
128 where serverLoop :: IO ()
131 -- TODO: option for port number
129 -- TODO: option for port number
132 serverLoop = withSocketsDo $
130 serverLoop = withSocketsDo $
133 do sock <- listenOnLocalhost $ PortNumber 4294
131 do sock <- listenOnLocalhost $ PortNumber 4294
134− i <- readMVar stvar
135− loop fn i sock
132+ loop fn orig sock
136
133
137 fn = case fn_in of
134 fn = case fn_in of
138 (f:_) -> f
135 (f:_) -> f
@@ -146,19 +143,16 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
146 host == "127.0.0.1")
143 host == "127.0.0.1")
147 then do
144 then do
148 cmd <- hGetLine h
145 cmd <- hGetLine h
149− takeMVar stvar
150− (ist', fn) <- processNetCmd stvar orig ist h fn cmd
146+ (ist', fn) <- processNetCmd orig ist h fn cmd
151− putMVar stvar ist'
152 hClose h
147 hClose h
153 loop fn ist' sock
148 loop fn ist' sock
154 else do
149 else do
155 putStrLn $ "Closing connection attempt from non-localhost " ++ host
150 putStrLn $ "Closing connection attempt from non-localhost " ++ host
156 hClose h
151 hClose h
157
152
158−processNetCmd :: MVar IState ->
159− IState -> IState -> Handle -> FilePath -> String ->
153+processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
160 IO (IState, FilePath)
154 IO (IState, FilePath)
161−processNetCmd stvar orig i h fn cmd
155+processNetCmd orig i h fn cmd
162 = do res <- case parseCmd i "(net)" cmd of
156 = do res <- case parseCmd i "(net)" cmd of
163 Failure err -> return (Left (Msg " invalid command"))
157 Failure err -> return (Left (Msg " invalid command"))
164 Success c -> runErrorT $ evalStateT (processNet fn c) i
158 Success c -> runErrorT $ evalStateT (processNet fn c) i
@@ -337,9 +331,9 @@ lit f = case splitExtension f of
337 (_, ".lidr") -> True
331 (_, ".lidr") -> True
338 _ -> False
332 _ -> False
339
333
340−processInput :: MVar IState -> String ->
334+processInput :: String ->
341 IState -> [FilePath] -> Idris (Maybe [FilePath])
335 IState -> [FilePath] -> Idris (Maybe [FilePath])
342−processInput stvar cmd orig inputs
336+processInput cmd orig inputs
343 = do i <- getIState
337 = do i <- getIState
344 let opts = idris_options i
338 let opts = idris_options i
345 let quiet = opt_quiet opts
339 let quiet = opt_quiet opts
@@ -1218,9 +1212,8 @@ idrisMain opts =
1218
1212
1219 when (runrepl && not idesl) $ do
1213 when (runrepl && not idesl) $ do
1220 initScript
1214 initScript
1221− stvar <- runIO $ newMVar ist
1222− startServer ist stvar inputs
1215+ startServer ist inputs
1223− runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs
1216+ runInputT (replSettings (Just historyFile)) $ repl ist inputs
1224 when (idesl) $ ideslaveStart ist inputs
1217 when (idesl) $ ideslaveStart ist inputs
1225 ok <- noErrors
1218 ok <- noErrors
1226 when (not ok) $ runIO (exitWith (ExitFailure 1))
1219 when (not ok) $ runIO (exitWith (ExitFailure 1))