@@ -58,8 +58,11 @@ import System.Directory
5858import System.IO
5959import Control.Monad
6060import Control.Monad.Trans.Error (ErrorT(..))
61−import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )
61+import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )
6262import Control.Monad.Trans ( lift )
63+import Control.Concurrent.MVar
64+import Network
65+import Control.Concurrent
6366import Data.Maybe
6467import Data.List
6568import Data.Char
@@ -72,12 +75,14 @@ import Debug.Trace
7275
7376-- | Run the REPL
7477repl :: IState -- ^ The initial state
78+ -> MVar IState -- ^ Server's MVar
7579 -> [FilePath] -- ^ The loaded modules
7680 -> InputT Idris ()
77−repl orig mods
81+repl orig stvar mods
7882 = H.catch
7983 (do let quiet = opt_quiet (idris_options orig)
8084 i <- lift getIState
85+ lift $ runIO $ swapMVar stvar i -- update shared state
8186 let colour = idris_colourRepl i
8287 let theme = idris_colourTheme i
8388 let prompt = if quiet
@@ -89,15 +94,74 @@ repl orig mods
8994 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
9095 return ()
9196 Just input -> H.catch
92− (do ms <- lift $ processInput input orig mods
97+ (do ms <- lift $ processInput stvar input orig mods
9398 case ms of
94− Just mods -> repl orig mods
99+ Just mods -> repl orig stvar mods
95100 Nothing -> return ())
96101 ctrlC)
97− ctrlC
102+ ctrlC
98103 where ctrlC :: SomeException -> InputT Idris ()
99104 ctrlC e = do lift $ iputStrLn (show e)
100− repl orig mods
105+ repl orig stvar mods
106+
107+-- | Run the REPL server
108+startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
109+startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
110+ return ()
111+ where serverLoop :: IO ()
112+ -- TODO: option for port number
113+ serverLoop = withSocketsDo $ do sock <- listenOn $ PortNumber 4294
114+ i <- readMVar stvar
115+ loop i sock
116+
117+ fn = case fn_in of
118+ (f:_) -> f
119+ _ -> ""
120+
121+ loop ist sock = do (h,_,_) <- accept sock
122+ cmd <- hGetLine h
123+ takeMVar stvar
124+ ist' <- processNetCmd stvar orig ist h fn cmd
125+ putMVar stvar ist'
126+ hClose h
127+ loop ist' sock
128+
129+processNetCmd :: MVar IState ->
130+ IState -> IState -> Handle -> FilePath -> String -> IO IState
131+processNetCmd stvar orig i h fn cmd
132+ = do res <- case parseCmd i "(net)" cmd of
133+ Failure err -> return (Left (Msg " invalid command"))
134+ Success c -> runErrorT $ evalStateT (processNet fn c) i
135+ case res of
136+ Right ist -> return ist
137+ Left err -> do hPutStrLn h (show err)
138+ return i
139+ where
140+ processNet fn Reload =
141+ do let ist = orig { idris_options = idris_options i
142+ , idris_colourTheme = idris_colourTheme i
143+ }
144+ putIState orig
145+ setOutH h
146+ mods <- loadInputs h [fn]
147+ ist <- getIState
148+ return ist
149+ processNet fn c = do process h fn c
150+ ist <- getIState
151+ return ist
152+
153+-- | Run a command on the server on localhost
154+runClient :: String -> IO ()
155+runClient str = withSocketsDo $ do
156+ h <- connectTo "localhost" (PortNumber 4294)
157+ hPutStrLn h str
158+ resp <- hGetResp "" h
159+ putStr resp
160+ hClose h
161+ where hGetResp acc h = do eof <- hIsEOF h
162+ if eof then return acc
163+ else do l <- hGetLine h
164+ hGetResp (acc ++ l ++ "\n") h
101165
102166-- | Run the IdeSlave
103167ideslaveStart :: IState -> [FilePath] -> Idris ()
@@ -126,7 +190,7 @@ ideslave orig mods
126190 Failure err -> iPrintError $ show (fixColour c err)
127191 Success (Prove n') -> do iPrintResult ""
128192 idrisCatch
129− (process fn (Prove n'))
193+ (process stdout fn (Prove n'))
130194 (\e -> getIState >>= iPrintError . flip pshow e)
131195 isetPrompt (mkPrompt mods)
132196 Success cmd -> idrisCatch
@@ -140,7 +204,7 @@ ideslave orig mods
140204 do clearErr
141205 putIState (orig { idris_options = idris_options i,
142206 idris_outputmode = (IdeSlave id) })
143− loadModule filename
207+ loadModule stdout filename
144208 iucheck
145209 isetPrompt (mkPrompt [filename])
146210
@@ -155,53 +219,53 @@ ideslave orig mods
155219 ideslave orig mods
156220
157221ideslaveProcess :: FilePath -> Command -> Idris ()
158−ideslaveProcess fn Help = process fn Help
159−ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)
222+ideslaveProcess fn Help = process stdout fn Help
223+ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
160224 iPrintResult "changed directory to"
161−ideslaveProcess fn (Eval t) = process fn (Eval t)
162−ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)
163−ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
164−ideslaveProcess fn (Check t) = process fn (Check t)
165−ideslaveProcess fn (DocStr n) = process fn (DocStr n)
166−ideslaveProcess fn Universes = process fn Universes
167−ideslaveProcess fn (Defn n) = do process fn (Defn n)
225+ideslaveProcess fn (Eval t) = process stdout fn (Eval t)
226+ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)
227+ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))
228+ideslaveProcess fn (Check t) = process stdout fn (Check t)
229+ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)
230+ideslaveProcess fn Universes = process stdout fn Universes
231+ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
168232 iPrintResult ""
169−ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)
170−ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)
233+ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
234+ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
171235 iPrintResult ""
172−ideslaveProcess fn (Info n) = process fn (Info n)
173−ideslaveProcess fn (Search t) = process fn (Search t)
174−ideslaveProcess fn (Spec t) = process fn (Spec t)
236+ideslaveProcess fn (Info n) = process stdout fn (Info n)
237+ideslaveProcess fn (Search t) = process stdout fn (Search t)
238+ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
175239-- RmProof and AddProof not supported!
176−ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
177−ideslaveProcess fn (HNF t) = process fn (HNF t)
178−--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
240+ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')
241+ideslaveProcess fn (HNF t) = process stdout fn (HNF t)
242+--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!
179243
180244--that most likely does not work, since we need to wrap
181245--input/output of the executed binary...
182−ideslaveProcess fn Execute = do process fn Execute
246+ideslaveProcess fn Execute = do process stdout fn Execute
183247 iPrintResult ""
184−ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)
248+ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)
185249 iPrintResult ""
186−ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)
250+ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)
187251 iPrintResult ""
188−ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)
189−ideslaveProcess fn (Missing n) = process fn (Missing n)
190−ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)
252+ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)
253+ideslaveProcess fn (Missing n) = process stdout fn (Missing n)
254+ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)
191255 iPrintResult ""
192−ideslaveProcess fn ListDynamic = do process fn ListDynamic
256+ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic
193257 iPrintResult ""
194−ideslaveProcess fn Metavars = process fn Metavars
195−ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
258+ideslaveProcess fn Metavars = process stdout fn Metavars
259+ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)
196260 iPrintResult ""
197−ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
261+ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)
198262 iPrintResult ""
199−ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
263+ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)
200264 iPrintResult ""
201−ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
265+ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)
202266 iPrintResult ""
203−ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)
204−ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
267+ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)
268+ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)
205269ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
206270
207271
@@ -215,8 +279,9 @@ lit f = case splitExtension f of
215279 (_, ".lidr") -> True
216280 _ -> False
217281
218−processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
219−processInput cmd orig inputs
282+processInput :: MVar IState -> String ->
283+ IState -> [FilePath] -> Idris (Maybe [FilePath])
284+processInput stvar cmd orig inputs
220285 = do i <- getIState
221286 let opts = idris_options i
222287 let quiet = opt_quiet opts
@@ -232,26 +297,27 @@ processInput cmd orig inputs
232297 , idris_colourTheme = idris_colourTheme i
233298 }
234299 clearErr
235− mods <- loadInputs inputs
300+ mods <- loadInputs stdout inputs
236301 return (Just inputs)
237302 Success (Load f) ->
238303 do putIState orig { idris_options = idris_options i
239304 , idris_colourTheme = idris_colourTheme i
240305 }
241306 clearErr
242− mod <- loadModule f
307+ mod <- loadModule stdout f
243308 return (Just [f])
244309 Success (ModImport f) ->
245310 do clearErr
246− fmod <- loadModule f
311+ fmod <- loadModule stdout f
247312 return (Just (inputs ++ [fmod]))
248− Success Edit -> do edit fn orig
313+ Success Edit -> do -- takeMVar stvar
314+ edit fn orig
249315 return (Just inputs)
250316 Success Proofs -> do proofs orig
251317 return (Just inputs)
252318 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")
253319 return Nothing
254− Success cmd -> do idrisCatch (process fn cmd)
320+ Success cmd -> do idrisCatch (process stdout fn cmd)
255321 (\e -> do msg <- showErr e ; iputStrLn msg)
256322 return (Just inputs)
257323
@@ -287,7 +353,7 @@ edit f orig
287353 putIState $ orig { idris_options = idris_options i
288354 , idris_colourTheme = idris_colourTheme i
289355 }
290− loadInputs [f]
356+ loadInputs stdout [f]
291357 iucheck
292358 return ()
293359 where getEditor env | Just ed <- lookup "EDITOR" env = ed
@@ -312,12 +378,12 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)
312378 = p : "" : prf : xs
313379insertScript prf (x : xs) = x : insertScript prf xs
314380
315−process :: FilePath -> Command -> Idris ()
316−process fn Help = iPrintResult displayHelp
317−process fn (ChangeDirectory f)
381+process :: Handle -> FilePath -> Command -> Idris ()
382+process h fn Help = iPrintResult displayHelp
383+process h fn (ChangeDirectory f)
318384 = do runIO $ setCurrentDirectory f
319385 return ()
320−process fn (Eval t)
386+process h fn (Eval t)
321387 = do (tm, ty) <- elabVal toplevel False t
322388 ctxt <- getContext
323389 ist <- getIState
@@ -329,9 +395,9 @@ process fn (Eval t)
329395 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
330396 imp <- impShow
331397 c <- colourise
332− iPrintResult (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
398+ ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
333399 showImp (Just ist) imp c (delab ist ty'))
334−process fn (ExecVal t)
400+process h fn (ExecVal t)
335401 = do ctxt <- getContext
336402 ist <- getIState
337403 (tm, ty) <- elabVal toplevel False t
@@ -340,19 +406,19 @@ process fn (ExecVal t)
340406 res <- execute tm
341407 imp <- impShow
342408 c <- colourise
343− iPrintResult (showImp (Just ist) imp c (delab ist res) ++ " : " ++
409+ ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++
344410 showImp (Just ist) imp c (delab ist ty'))
345−process fn (Check (PRef _ n))
411+process h fn (Check (PRef _ n))
346412 = do ctxt <- getContext
347413 ist <- getIState
348414 imp <- impShow
349415 c <- colourise
350416 case lookupNames n ctxt of
351− ts@(_:_) -> do mapM_ (\n -> iputStrLn $ showName (Just ist) [] False c n ++ " : " ++
417+ ts@(_:_) -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++
352418 showImp (Just ist) imp c (delabTy ist n)) ts
353− iPrintResult ""
354− [] -> iPrintError $ "No such variable " ++ show n
355−process fn (Check t)
419+ ihPrintResult h ""
420+ [] -> ihPrintError h $ "No such variable " ++ show n
421+process h fn (Check t)
356422 = do (tm, ty) <- elabVal toplevel False t
357423 ctxt <- getContext
358424 ist <- getIState
@@ -360,11 +426,12 @@ process fn (Check t)
360426 c <- colourise
361427 let ty' = normaliseC ctxt [] ty
362428 case tm of
363− TType _ -> iPrintResult ("Type : Type 1")
364− _ -> iPrintResult (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
365− showImp (Just ist) imp c (delab ist ty))
429+ TType _ -> ihPrintResult h ("Type : Type 1")
430+ _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
431+ showImp (Just ist) imp c (delab ist ty))
366432
367−process fn (DocStr n) = do i <- getIState
433+process h fn (DocStr n)
434+ = do i <- getIState
368435 case lookupCtxtName n (idris_docstrings i) of
369436 [] -> iPrintError $ "No documentation for " ++ show n
370437 ns -> do mapM_ showDoc ns
@@ -372,7 +439,8 @@ process fn (DocStr n) = do i <- getIState
372439 where showDoc (n, d)
373440 = do doc <- getDocs n
374441 iputStrLn $ show doc
375−process fn Universes = do i <- getIState
442+process h fn Universes
443+ = do i <- getIState
376444 let cs = idris_constraints i
377445-- iputStrLn $ showSep "\n" (map show cs)
378446 iputStrLn $ show (map fst cs)
@@ -381,7 +449,8 @@ process fn Universes = do i <- getIState
381449 case ucheck cs of
382450 Error e -> iPrintError $ pshow i e
383451 OK _ -> iPrintResult "Universes OK"
384−process fn (Defn n) = do i <- getIState
452+process h fn (Defn n)
453+ = do i <- getIState
385454 iputStrLn "Compiled patterns:\n"
386455 iputStrLn $ show (lookupDef n (tt_ctxt i))
387456 case lookupCtxt n (idris_patdefs i) of
@@ -395,12 +464,13 @@ process fn (Defn n) = do i <- getIState
395464 = do c <- colourise
396465 iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++
397466 showImp (Just i) True c (delab i rhs))
398−process fn (TotCheck n) = do i <- getIState
467+process h fn (TotCheck n)
468+ = do i <- getIState
399469 case lookupTotal n (tt_ctxt i) of
400470 [t] -> iPrintResult (showTotal t i)
401471 _ -> do iPrintError ""
402472 return ()
403−process fn (DebugInfo n)
473+process h fn (DebugInfo n)
404474 = do i <- getIState
405475 let oi = lookupCtxtName n (idris_optimisation i)
406476 when (not (null oi)) $ iputStrLn (show oi)
@@ -418,29 +488,37 @@ process fn (DebugInfo n)
418488 iputStrLn $ "Size change: " ++ show sc
419489 when (not (null cg')) $ do iputStrLn "Call graph:\n"
420490 iputStrLn (show cg')
421−process fn (Info n) = do i <- getIState
491+process h fn (Info n)
492+ = do i <- getIState
422493 case lookupCtxt n (idris_classes i) of
423494 [c] -> classInfo c
424495 _ -> iPrintError "Not a class"
425−process fn (Search t) = iPrintError "Not implemented"
426−process fn (CaseSplit n t)
496+process h fn (Search t) = iPrintError "Not implemented"
497+process h fn (CaseSplit n t)
427498 = do tms <- split n t
428499 iputStrLn (showSep "\n" (map show tms))
429−process fn (CaseSplitAt l n)
500+process h fn (CaseSplitAt updatefile l n)
430501 = do src <- runIO $ readFile fn
431502 res <- splitOnLine l n fn
432503 iLOG (showSep "\n" (map show res))
433504 let (before, (ap : later)) = splitAt (l-1) (lines src)
434− iputStrLn (showSep "\n" (replaceSplits ap res))
505+ let new = concat (replaceSplits ap res)
506+ ihputStrLn h new
507+ if updatefile then
508+ do let fb = fn ++ "~" -- make a backup!
509+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)
510+ runIO $ copyFile fb fn
511+ else return ()
435512
436513
437−process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
514+process h fn (Spec t)
515+ = do (tm, ty) <- elabVal toplevel False t
438516 ctxt <- getContext
439517 ist <- getIState
440518 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
441519 iPrintResult (show (delab ist tm'))
442520
443−process fn (RmProof n')
521+process h fn (RmProof n')
444522 = do i <- getIState
445523 n <- resolveProof n'
446524 let proofs = proof_list i
@@ -456,7 +534,7 @@ process fn (RmProof n')
456534 let ms = idris_metavars i
457535 putIState $ i { idris_metavars = n : ms }
458536
459−process fn' (AddProof prf)
537+process h fn' (AddProof prf)
460538 = do fn <- do
461539 ex <- runIO $ doesFileExist fn'
462540 let fnExt = fn' <.> "idr"
@@ -485,7 +563,7 @@ process fn' (AddProof prf)
485563 iputStrLn $ "Added proof " ++ show n
486564 where ls = (lines prog)
487565
488−process fn (ShowProof n')
566+process h fn (ShowProof n')
489567 = do i <- getIState
490568 n <- resolveProof n'
491569 let proofs = proof_list i
@@ -493,7 +571,7 @@ process fn (ShowProof n')
493571 Nothing -> iPrintError "No proof to show"
494572 Just p -> iPrintResult $ showProof False n p
495573
496−process fn (Prove n')
574+process h fn (Prove n')
497575 = do ctxt <- getContext
498576 ist <- getIState
499577 n <- case lookupNames n' ctxt of
@@ -507,23 +585,27 @@ process fn (Prove n')
507585 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
508586 mapM_ checkDeclTotality (idris_totcheck i)
509587
510−process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
588+process h fn (HNF t)
589+ = do (tm, ty) <- elabVal toplevel False t
511590 ctxt <- getContext
512591 ist <- getIState
513592 let tm' = hnf ctxt [] tm
514593 iPrintResult (show (delab ist tm'))
515−process fn (TestInline t) = do (tm, ty) <- elabVal toplevel False t
594+process h fn (TestInline t)
595+ = do (tm, ty) <- elabVal toplevel False t
516596 ctxt <- getContext
517597 ist <- getIState
518598 let tm' = inlineTerm ist tm
519599 imp <- impShow
520600 c <- colourise
521601 iPrintResult (showImp (Just ist) imp c (delab ist tm'))
522−process fn TTShell = do ist <- getIState
602+process h fn TTShell
603+ = do ist <- getIState
523604 let shst = initState (tt_ctxt ist)
524605 runShell shst
525606 return ()
526−process fn Execute = do (m, _) <- elabVal toplevel False
607+process h fn Execute
608+ = do (m, _) <- elabVal toplevel False
527609 (PApp fc
528610 (PRef fc (UN "run__IO"))
529611 [pexp $ PRef fc (NS (UN "main") ["Main"])])
@@ -535,19 +617,19 @@ process fn Execute = do (m, _) <- elabVal toplevel False
535617 runIO $ system tmpn
536618 return ()
537619 where fc = fileFC "main"
538−process fn (Compile codegen f)
620+process h fn (Compile codegen f)
539621 = do (m, _) <- elabVal toplevel False
540622 (PApp fc (PRef fc (UN "run__IO"))
541623 [pexp $ PRef fc (NS (UN "main") ["Main"])])
542624 compile codegen f m
543625 where fc = fileFC "main"
544−process fn (LogLvl i) = setLogLevel i
626+process h fn (LogLvl i) = setLogLevel i
545627-- Elaborate as if LHS of a pattern (debug command)
546−process fn (Pattelab t)
628+process h fn (Pattelab t)
547629 = do (tm, ty) <- elabVal toplevel True t
548630 iPrintResult $ show tm ++ "\n\n : " ++ show ty
549631
550−process fn (Missing n)
632+process h fn (Missing n)
551633 = do i <- getIState
552634 c <- colourise
553635 case lookupCtxt n (idris_patdefs i) of
@@ -555,7 +637,8 @@ process fn (Missing n)
555637 [(_, tms)] ->
556638 iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))
557639 _ -> iPrintError $ "Ambiguous name"
558−process fn (DynamicLink l) = do i <- getIState
640+process h fn (DynamicLink l)
641+ = do i <- getIState
559642 let lib = trim l
560643 handle <- lift . lift $ tryLoadLib lib
561644 case handle of
@@ -566,33 +649,35 @@ process fn (DynamicLink l) = do i <- getIState
566649 return ()
567650 else putIState $ i { idris_dynamic_libs = x:libs }
568651 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
569−process fn ListDynamic = do i <- getIState
652+process h fn ListDynamic
653+ = do i <- getIState
570654 iputStrLn "Dynamic libraries:"
571655 showLibs $ idris_dynamic_libs i
572656 where showLibs [] = return ()
573657 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
574−process fn Metavars
658+process h fn Metavars
575659 = do ist <- getIState
576660 let mvs = idris_metavars ist \\ primDefs
577661 case mvs of
578662 [] -> iPrintError "No global metavariables to solve"
579663 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
580−process fn NOP = return ()
581−
582−process fn (SetOpt ErrContext) = setErrContext True
583−process fn (UnsetOpt ErrContext) = setErrContext False
584−process fn (SetOpt ShowImpl) = setImpShow True
585−process fn (UnsetOpt ShowImpl) = setImpShow False
586−
587−process fn (SetOpt _) = iPrintError "Not a valid option"
588−process fn (UnsetOpt _) = iPrintError "Not a valid option"
589−process fn (SetColour ty c) = setColour ty c
590−process fn ColourOn = do ist <- getIState
664+process h fn NOP = return ()
665+
666+process h fn (SetOpt ErrContext) = setErrContext True
667+process h fn (UnsetOpt ErrContext) = setErrContext False
668+process h fn (SetOpt ShowImpl) = setImpShow True
669+process h fn (UnsetOpt ShowImpl) = setImpShow False
670+
671+process h fn (SetOpt _) = iPrintError "Not a valid option"
672+process h fn (UnsetOpt _) = iPrintError "Not a valid option"
673+process h fn (SetColour ty c) = setColour ty c
674+process h fn ColourOn
675+ = do ist <- getIState
591676 putIState $ ist { idris_colourRepl = True }
592−process fn ColourOff = do ist <- getIState
677+process h fn ColourOff
678+ = do ist <- getIState
593679 putIState $ ist { idris_colourRepl = False }
594680
595−
596681classInfo :: ClassInfo -> Idris ()
597682classInfo ci = do iputStrLn "Methods:\n"
598683 mapM_ dumpMethod (class_methods ci)
@@ -641,6 +726,7 @@ parseArgs :: [String] -> [Opt]
641726parseArgs [] = []
642727parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
643728parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
729+parseArgs ("--client":ns) = [Client (showSep " " ns)]
644730parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
645731parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
646732parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
@@ -709,8 +795,8 @@ idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
709795 Right ist -> return ()
710796
711797
712−loadInputs :: [FilePath] -> Idris ()
713−loadInputs inputs
798+loadInputs :: Handle -> [FilePath] -> Idris ()
799+loadInputs h inputs
714800 = do ist <- getIState
715801 -- if we're in --check and not outputting anything, don't bother
716802 -- loading, as it gets really slow if there's lots of modules in
@@ -764,7 +850,7 @@ loadInputs inputs
764850 where -- load all files, stop if any fail
765851 tryLoad :: [IFileType] -> Idris ()
766852 tryLoad [] = return ()
767− tryLoad (f : fs) = do loadFromIFile f
853+ tryLoad (f : fs) = do loadFromIFile h f
768854 inew <- getIState
769855 case errLine inew of
770856 Nothing -> tryLoad fs
@@ -837,19 +923,19 @@ idrisMain opts =
837923 addPkgDir "base"
838924 mapM_ addPkgDir pkgdirs
839925 elabPrims
840− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
926+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
841927 return ()
842928 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
843929 ist <- getIState
844930
845− loadInputs inputs
931+ loadInputs stdout inputs
846932
847933 runIO $ hSetBuffering stdout LineBuffering
848934
849935 ok <- noErrors
850936 when ok $ case output of
851937 [] -> return ()
852− (o:_) -> process "" (Compile cgn o)
938+ (o:_) -> process stdout "" (Compile cgn o)
853939 case script of
854940 Nothing -> return ()
855941 Just expr -> execScript expr
@@ -857,7 +943,9 @@ idrisMain opts =
857943 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
858944
859945 when runrepl $ initScript
860− when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs
946+ stvar <- runIO $ newMVar ist
947+ when runrepl $ startServer ist stvar inputs
948+ when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs
861949 when (idesl) $ ideslaveStart ist inputs
862950 ok <- noErrors
863951 when (not ok) $ runIO (exitWith (ExitFailure 1))
@@ -925,7 +1013,7 @@ initScript = do script <- getInitScript
9251013 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
9261014 Success Proofs -> proofs i
9271015 Success Quit -> iPrintError "Init scripts cannot quit Idris"
928− Success cmd -> process [] cmd
1016+ Success cmd -> process stdout [] cmd
9291017
9301018getFile :: Opt -> Maybe String
9311019getFile (Filename str) = Just str