on master help sign in
Remove MVar from REPL

Because we don't actually share state...

commitef0b6ec56335126593681ceb6b128bfbe69048bc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 Jan 2014, 10:48 (13 years ago) parentfa364ca
1 file changed+15−22
src/Idris/REPL.hs+15−22
src/Idris/REPL.hs+15−22
@@ -77,14 +77,12 @@ import Debug.Trace
7777
7878-- | Run the REPL
7979repl :: IState -- ^ The initial state
80− -> MVar IState -- ^ Server's MVar
8180 -> [FilePath] -- ^ The loaded modules
8281 -> InputT Idris ()
83−repl orig stvar mods
82+repl orig mods
8483 = H.catch
8584 (do let quiet = opt_quiet (idris_options orig)
8685 i <- lift getIState
87− lift $ runIO $ swapMVar stvar i -- update shared state
8886 let colour = idris_colourRepl i
8987 let theme = idris_colourTheme i
9088 let mvs = idris_metavars i
@@ -98,15 +96,15 @@ repl orig stvar mods
9896 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
9997 return ()
10098 Just input -> H.catch
101− (do ms <- lift $ processInput stvar input orig mods
99+ (do ms <- lift $ processInput input orig mods
102100 case ms of
103− Just mods -> repl orig stvar mods
101+ Just mods -> repl orig mods
104102 Nothing -> return ())
105103 ctrlC)
106104 ctrlC
107105 where ctrlC :: SomeException -> InputT Idris ()
108106 ctrlC e = do lift $ iputStrLn (show e)
109− repl orig stvar mods
107+ repl orig mods
110108
111109 showMVs c thm [] = ""
112110 showMVs c thm ms = "Metavariables: " ++
@@ -124,15 +122,14 @@ repl orig stvar mods
124122 else show n
125123
126124-- | Run the REPL server
127−startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
128−startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
129− return ()
125+startServer :: IState -> [FilePath] -> Idris ()
126+startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
127+ return ()
130128 where serverLoop :: IO ()
131129 -- TODO: option for port number
132130 serverLoop = withSocketsDo $
133131 do sock <- listenOnLocalhost $ PortNumber 4294
134− i <- readMVar stvar
135− loop fn i sock
132+ loop fn orig sock
136133
137134 fn = case fn_in of
138135 (f:_) -> f
@@ -146,19 +143,16 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
146143 host == "127.0.0.1")
147144 then do
148145 cmd <- hGetLine h
149− takeMVar stvar
150− (ist', fn) <- processNetCmd stvar orig ist h fn cmd
151− putMVar stvar ist'
146+ (ist', fn) <- processNetCmd orig ist h fn cmd
152147 hClose h
153148 loop fn ist' sock
154149 else do
155150 putStrLn $ "Closing connection attempt from non-localhost " ++ host
156151 hClose h
157152
158−processNetCmd :: MVar IState ->
159− IState -> IState -> Handle -> FilePath -> String ->
153+processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
160154 IO (IState, FilePath)
161−processNetCmd stvar orig i h fn cmd
155+processNetCmd orig i h fn cmd
162156 = do res <- case parseCmd i "(net)" cmd of
163157 Failure err -> return (Left (Msg " invalid command"))
164158 Success c -> runErrorT $ evalStateT (processNet fn c) i
@@ -337,9 +331,9 @@ lit f = case splitExtension f of
337331 (_, ".lidr") -> True
338332 _ -> False
339333
340−processInput :: MVar IState -> String ->
334+processInput :: String ->
341335 IState -> [FilePath] -> Idris (Maybe [FilePath])
342−processInput stvar cmd orig inputs
336+processInput cmd orig inputs
343337 = do i <- getIState
344338 let opts = idris_options i
345339 let quiet = opt_quiet opts
@@ -1218,9 +1212,8 @@ idrisMain opts =
12181212
12191213 when (runrepl && not idesl) $ do
12201214 initScript
1221− stvar <- runIO $ newMVar ist
1222− startServer ist stvar inputs
1223− runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs
1215+ startServer ist inputs
1216+ runInputT (replSettings (Just historyFile)) $ repl ist inputs
12241217 when (idesl) $ ideslaveStart ist inputs
12251218 ok <- noErrors
12261219 when (not ok) $ runIO (exitWith (ExitFailure 1))