@@ -187,12 +187,18 @@ processNetCmd orig i h fn cmd
187187 setOutH h
188188 setQuiet True
189189 setVerbose False
190− mods <- loadInputs h [f] toline
190+ mods <- loadInputs [f] toline
191191 ist <- getIState
192192 return (ist, f)
193− processNet fn c = do process h fn c
193+ processNet fn c = do process fn c
194194 ist <- getIState
195195 return (ist, fn)
196+ setOutH :: Handle -> Idris ()
197+ setOutH h =
198+ do ist <- getIState
199+ case idris_outputmode ist of
200+ RawOutput _ -> putIState ist {idris_outputmode = RawOutput h}
201+ IdeSlave n _ -> putIState ist {idris_outputmode = IdeSlave n h}
196202
197203-- | Run a command on the server on localhost
198204runClient :: String -> IO ()
@@ -208,7 +214,7 @@ runClient str = withSocketsDo $ do
208214 else do l <- hGetLine h
209215 hGetResp (acc ++ l ++ "\n") h
210216
211−initIdeslaveSocket :: IO (Handle)
217+initIdeslaveSocket :: IO Handle
212218initIdeslaveSocket = do
213219 (sock, port) <- listenOnLocalhostAnyPort
214220 putStrLn $ show port
@@ -276,7 +282,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =
276282 Failure err -> iPrintError $ show (fixColour c err)
277283 Success (Prove n') ->
278284 idrisCatch
279− (do process stdout fn (Prove n')
285+ (do process fn (Prove n')
280286 isetPrompt (mkPrompt mods)
281287 case idris_outputmode i of
282288 IdeSlave n h -> -- signal completion of proof to ide
@@ -292,10 +298,10 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =
292298 runIO . hPutStrLn h $
293299 IdeSlave.convSExp "abandon-proof" "Abandoned" n
294300 _ -> return ()
295− ihRenderError h $ pprintErr ist e)
301+ iRenderError $ pprintErr ist e)
296302 Success cmd -> idrisCatch
297303 (ideslaveProcess fn cmd)
298− (\e -> getIState >>= ihRenderError h . flip pprintErr e)
304+ (\e -> getIState >>= iRenderError . flip pprintErr e)
299305runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =
300306 do (unused, compls) <- replCompletion (reverse str, "")
301307 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
@@ -307,7 +313,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =
307313 clearErr
308314 putIState (orig { idris_options = idris_options i,
309315 idris_outputmode = (IdeSlave id h) })
310− loadInputs stdout [filename] toline
316+ loadInputs [filename] toline
311317 isetPrompt (mkPrompt [filename])
312318 -- Report either success or failure
313319 i <- getIState
@@ -323,7 +329,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =
323329runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =
324330 case splitName name of
325331 Left err -> iPrintError err
326− Right n -> process stdout "(ideslave)"
332+ Right n -> process "(ideslave)"
327333 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
328334 where splitName :: String -> Either String Name
329335 splitName s = case reverse $ splitOn "." s of
@@ -332,29 +338,29 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =
332338 (n:ns) -> Right $ sNS (sUN n) ns
333339runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =
334340 case parseConst orig name of
335− Success c -> process stdout "(ideslave)" (DocStr (Right c))
341+ Success c -> process "(ideslave)" (DocStr (Right c))
336342 Failure _ ->
337343 case splitName name of
338344 Left err -> iPrintError err
339− Right n -> process stdout "(ideslave)" (DocStr (Left n))
345+ Right n -> process "(ideslave)" (DocStr (Left n))
340346runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =
341− process stdout fn (CaseSplitAt False line (sUN name))
347+ process fn (CaseSplitAt False line (sUN name))
342348runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =
343− process stdout fn (AddClauseFrom False line (sUN name))
349+ process fn (AddClauseFrom False line (sUN name))
344350runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =
345− process stdout fn (AddProofClauseFrom False line (sUN name))
351+ process fn (AddProofClauseFrom False line (sUN name))
346352runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =
347− process stdout fn (AddMissing False line (sUN name))
353+ process fn (AddMissing False line (sUN name))
348354runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =
349− process stdout fn (MakeWith False line (sUN name))
355+ process fn (MakeWith False line (sUN name))
350356runIdeSlaveCommand h id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =
351− doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth
357+ doProofSearch fn False r line (sUN name) (map sUN hints) depth
352358runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =
353359 case splitName name of
354360 Left err -> iPrintError err
355− Right n -> process stdout fn (MakeLemma False line n)
361+ Right n -> process fn (MakeLemma False line n)
356362runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =
357− process stdout fn (Apropos a)
363+ process fn (Apropos a)
358364runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =
359365 do ist <- getIState
360366 let opts = idris_options ist
@@ -499,70 +505,70 @@ splitName s = case reverse $ splitOn "." s of
499505 (n:ns) -> Right $ sNS (sUN n) ns
500506
501507ideslaveProcess :: FilePath -> Command -> Idris ()
502−ideslaveProcess fn Warranty = process stdout fn Warranty
503−ideslaveProcess fn Help = process stdout fn Help
504−ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
508+ideslaveProcess fn Warranty = process fn Warranty
509+ideslaveProcess fn Help = process fn Help
510+ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)
505511 iPrintResult "changed directory to"
506−ideslaveProcess fn (Eval t) = process stdout fn (Eval t)
507−ideslaveProcess fn (NewDefn decls) = do process stdout fn (NewDefn decls)
512+ideslaveProcess fn (Eval t) = process fn (Eval t)
513+ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)
508514 iPrintResult "defined"
509−ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)
510−ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))
511−ideslaveProcess fn (Check t) = process stdout fn (Check t)
512−ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)
513−ideslaveProcess fn Universes = process stdout fn Universes
514−ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
515+ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)
516+ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
517+ideslaveProcess fn (Check t) = process fn (Check t)
518+ideslaveProcess fn (DocStr n) = process fn (DocStr n)
519+ideslaveProcess fn Universes = process fn Universes
520+ideslaveProcess fn (Defn n) = do process fn (Defn n)
515521 iPrintResult ""
516−ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
517−ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
522+ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)
523+ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)
518524 iPrintResult ""
519−ideslaveProcess fn (Search t) = process stdout fn (Search t)
520−ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
525+ideslaveProcess fn (Search t) = process fn (Search t)
526+ideslaveProcess fn (Spec t) = process fn (Spec t)
521527-- RmProof and AddProof not supported!
522−ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')
523−ideslaveProcess fn (HNF t) = process stdout fn (HNF t)
524−--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!
525−ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)
528+ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
529+ideslaveProcess fn (HNF t) = process fn (HNF t)
530+--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
531+ideslaveProcess fn (TestInline t) = process fn (TestInline t)
526532
527−ideslaveProcess fn Execute = do process stdout fn Execute
533+ideslaveProcess fn Execute = do process fn Execute
528534 iPrintResult ""
529−ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)
535+ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)
530536 iPrintResult ""
531−ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)
537+ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)
532538 iPrintResult ""
533−ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)
534−ideslaveProcess fn (Missing n) = process stdout fn (Missing n)
535−ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)
539+ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)
540+ideslaveProcess fn (Missing n) = process fn (Missing n)
541+ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)
536542 iPrintResult ""
537−ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic
543+ideslaveProcess fn ListDynamic = do process fn ListDynamic
538544 iPrintResult ""
539−ideslaveProcess fn Metavars = process stdout fn Metavars
540−ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)
545+ideslaveProcess fn Metavars = process fn Metavars
546+ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
541547 iPrintResult ""
542−ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)
548+ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
543549 iPrintResult ""
544−ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)
550+ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
545551 iPrintResult ""
546−ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)
552+ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
547553 iPrintResult ""
548−ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)
554+ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)
549555 iPrintResult ""
550−ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)
556+ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)
551557 iPrintResult ""
552−ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)
553−ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)
554−ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)
555−ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)
556−ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
557−ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
558−ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)
559−ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)
560−ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)
558+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)
559+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
560+ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)
561+ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)
562+ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)
563+ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)
564+ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
565+ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
566+ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
561567 iPrintResult ""
562−ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)
568+ideslaveProcess fn (Apropos a) = do process fn (Apropos a)
563569 iPrintResult ""
564−ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)
565−ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)
570+ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)
571+ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)
566572ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
567573
568574
@@ -594,18 +600,18 @@ processInput cmd orig inputs
594600 , idris_colourTheme = idris_colourTheme i
595601 }
596602 clearErr
597− mods <- loadInputs stdout inputs Nothing
603+ mods <- loadInputs inputs Nothing
598604 return (Just inputs)
599605 Success (Load f toline) ->
600606 do putIState orig { idris_options = idris_options i
601607 , idris_colourTheme = idris_colourTheme i
602608 }
603609 clearErr
604− mod <- loadInputs stdout [f] toline
610+ mod <- loadInputs [f] toline
605611 return (Just [f])
606612 Success (ModImport f) ->
607613 do clearErr
608− fmod <- loadModule stdout f
614+ fmod <- loadModule f
609615 return (Just (inputs ++ [fmod]))
610616 Success Edit -> do -- takeMVar stvar
611617 edit fn orig
@@ -614,7 +620,7 @@ processInput cmd orig inputs
614620 return (Just inputs)
615621 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")
616622 return Nothing
617− Success cmd -> do idrisCatch (process stdout fn cmd)
623+ Success cmd -> do idrisCatch (process fn cmd)
618624 (\e -> do msg <- showErr e ; iputStrLn msg)
619625 return (Just inputs)
620626
@@ -650,7 +656,7 @@ edit f orig
650656 putIState $ orig { idris_options = idris_options i
651657 , idris_colourTheme = idris_colourTheme i
652658 }
653− loadInputs stdout [f] Nothing
659+ loadInputs [f] Nothing
654660-- clearOrigPats
655661 iucheck
656662 return ()
@@ -676,13 +682,13 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)
676682 = p : "" : prf : xs
677683insertScript prf (x : xs) = x : insertScript prf xs
678684
679−process :: Handle -> FilePath -> Command -> Idris ()
680−process h fn Help = iPrintResult displayHelp
681−process h fn Warranty = iPrintResult warranty
682−process h fn (ChangeDirectory f)
685+process :: FilePath -> Command -> Idris ()
686+process fn Help = iPrintResult displayHelp
687+process fn Warranty = iPrintResult warranty
688+process fn (ChangeDirectory f)
683689 = do runIO $ setCurrentDirectory f
684690 return ()
685−process h fn (Eval t)
691+process fn (Eval t)
686692 = withErrorReflection $ do logLvl 5 $ show t
687693 (tm, ty) <- elabVal recinfo ERHS t
688694 ctxt <- getContext
@@ -695,10 +701,10 @@ process h fn (Eval t)
695701 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
696702 let tmDoc = pprintDelab ist tm'
697703 tyDoc = pprintDelab ist ty'
698− ihPrintTermWithType h tmDoc tyDoc
704+ iPrintTermWithType tmDoc tyDoc
699705
700706
701−process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ show namedGroups) >> mapM_ defineName namedGroups where
707+process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ show namedGroups) >> mapM_ defineName namedGroups where
702708 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls
703709 getName :: PDecl -> Maybe Name
704710 getName (PTy docs argdocs syn fc opts name ty) = Just name
@@ -729,7 +735,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
729735 getRHS (PClauseR fc with rhs whereBlock) = rhs
730736 getRHS (PWithR fc with rhs whereBlock) = rhs
731737
732−process h fn (ExecVal t)
738+process fn (ExecVal t)
733739 = do ctxt <- getContext
734740 ist <- getIState
735741 (tm, ty) <- elabVal recinfo ERHS t
@@ -738,19 +744,19 @@ process h fn (ExecVal t)
738744 res <- execute tm
739745 let (resOut, tyOut) = (prettyIst ist (delab ist res),
740746 prettyIst ist (delab ist ty'))
741− ihPrintTermWithType h resOut tyOut
747+ iPrintTermWithType resOut tyOut
742748
743−process h fn (Check (PRef _ n))
749+process fn (Check (PRef _ n))
744750 = do ctxt <- getContext
745751 ist <- getIState
746752 let ppo = ppOptionIst ist
747753 case lookupNames n ctxt of
748754 ts@(t:_) ->
749755 case lookup t (idris_metavars ist) of
750− Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
756+ Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $
751757 showMetavarInfo ppo ist n i
752− Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
753− [] -> ihPrintError h $ "No such variable " ++ show n
758+ Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)
759+ [] -> iPrintError $ "No such variable " ++ show n
754760 where
755761 showMetavarInfo ppo ist n i
756762 = case lookupTy n (tt_ctxt ist) of
@@ -775,7 +781,7 @@ process h fn (Check (PRef _ n))
775781 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
776782
777783
778−process h fn (Check t)
784+process fn (Check t)
779785 = do (tm, ty) <- elabVal recinfo ERHS t
780786 ctxt <- getContext
781787 ist <- getIState
@@ -783,24 +789,24 @@ process h fn (Check t)
783789 ty' = normaliseC ctxt [] ty
784790 case tm of
785791 TType _ ->
786− ihPrintTermWithType h (prettyIst ist PType) type1Doc
787− _ -> ihPrintTermWithType h (pprintDelab ist tm)
788− (pprintDelab ist ty)
792+ iPrintTermWithType (prettyIst ist PType) type1Doc
793+ _ -> iPrintTermWithType (pprintDelab ist tm)
794+ (pprintDelab ist ty)
789795
790−process h fn (DocStr (Left n))
796+process fn (DocStr (Left n))
791797 = do ist <- getIState
792798 case lookupCtxtName n (idris_docstrings ist) of
793799 [] -> iPrintError $ "No documentation for " ++ show n
794800 ns -> do toShow <- mapM (showDoc ist) ns
795− ihRenderResult h (vsep toShow)
801+ iRenderResult (vsep toShow)
796802 where showDoc ist (n, d) = do doc <- getDocs n
797803 return $ pprintDocs ist doc
798804
799−process h fn (DocStr (Right c))
805+process fn (DocStr (Right c))
800806 = do ist <- getIState
801− ihRenderResult h $ pprintConstDocs ist c (constDocs c)
807+ iRenderResult $ pprintConstDocs ist c (constDocs c)
802808
803−process h fn Universes
809+process fn Universes
804810 = do i <- getIState
805811 let cs = idris_constraints i
806812-- iputStrLn $ showSep "\n" (map show cs)
@@ -810,7 +816,7 @@ process h fn Universes
810816 case ucheck cs of
811817 Error e -> iPrintError $ pshow i e
812818 OK _ -> iPrintResult "Universes OK"
813−process h fn (Defn n)
819+process fn (Defn n)
814820 = do i <- getIState
815821 iputStrLn "Compiled patterns:\n"
816822 iputStrLn $ show (lookupDef n (tt_ctxt i))
@@ -825,20 +831,20 @@ process h fn (Defn n)
825831 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
826832 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
827833 showTm i' (delab i rhs))
828−process h fn (TotCheck n)
834+process fn (TotCheck n)
829835 = do i <- getIState
830836 case lookupNameTotal n (tt_ctxt i) of
831− [] -> ihPrintError h $ "Unknown operator " ++ show n
837+ [] -> iPrintError $ "Unknown operator " ++ show n
832838 ts -> do ist <- getIState
833839 c <- colourise
834840 let ppo = ppOptionIst ist
835841 let showN = showName (Just ist) [] ppo c
836− ihPrintResult h . concat . intersperse "\n" .
842+ iPrintResult . concat . intersperse "\n" .
837843 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
838844 ts
839845
840846
841−process h fn (DebugInfo n)
847+process fn (DebugInfo n)
842848 = do i <- getIState
843849 let oi = lookupCtxtName n (idris_optimisation i)
844850 when (not (null oi)) $ iputStrLn (show oi)
@@ -855,29 +861,29 @@ process h fn (DebugInfo n)
855861 iputStrLn $ "Size change: " ++ show sc
856862 when (not (null cg')) $ do iputStrLn "Call graph:\n"
857863 iputStrLn (show cg')
858−process h fn (Search t) = searchByType h t
859−process h fn (CaseSplitAt updatefile l n)
860− = caseSplitAt h fn updatefile l n
861−process h fn (AddClauseFrom updatefile l n)
862− = addClauseFrom h fn updatefile l n
863−process h fn (AddProofClauseFrom updatefile l n)
864− = addProofClauseFrom h fn updatefile l n
865−process h fn (AddMissing updatefile l n)
866− = addMissing h fn updatefile l n
867−process h fn (MakeWith updatefile l n)
868− = makeWith h fn updatefile l n
869−process h fn (MakeLemma updatefile l n)
870− = makeLemma h fn updatefile l n
871−process h fn (DoProofSearch updatefile rec l n hints)
872− = doProofSearch h fn updatefile rec l n hints Nothing
873−process h fn (Spec t)
864+process fn (Search t) = searchByType t
865+process fn (CaseSplitAt updatefile l n)
866+ = caseSplitAt fn updatefile l n
867+process fn (AddClauseFrom updatefile l n)
868+ = addClauseFrom fn updatefile l n
869+process fn (AddProofClauseFrom updatefile l n)
870+ = addProofClauseFrom fn updatefile l n
871+process fn (AddMissing updatefile l n)
872+ = addMissing fn updatefile l n
873+process fn (MakeWith updatefile l n)
874+ = makeWith fn updatefile l n
875+process fn (MakeLemma updatefile l n)
876+ = makeLemma fn updatefile l n
877+process fn (DoProofSearch updatefile rec l n hints)
878+ = doProofSearch fn updatefile rec l n hints Nothing
879+process fn (Spec t)
874880 = do (tm, ty) <- elabVal recinfo ERHS t
875881 ctxt <- getContext
876882 ist <- getIState
877883 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
878884 iPrintResult (show (delab ist tm'))
879885
880−process h fn (RmProof n')
886+process fn (RmProof n')
881887 = do i <- getIState
882888 n <- resolveProof n'
883889 let proofs = proof_list i
@@ -893,7 +899,7 @@ process h fn (RmProof n')
893899 let ms = idris_metavars i
894900 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
895901
896−process h fn' (AddProof prf)
902+process fn' (AddProof prf)
897903 = do fn <- do
898904 let fn'' = takeWhile (/= ' ') fn'
899905 ex <- runIO $ doesFileExist fn''
@@ -923,7 +929,7 @@ process h fn' (AddProof prf)
923929 iputStrLn $ "Added proof " ++ show n
924930 where ls = (lines prog)
925931
926−process h fn (ShowProof n')
932+process fn (ShowProof n')
927933 = do i <- getIState
928934 n <- resolveProof n'
929935 let proofs = proof_list i
@@ -931,7 +937,7 @@ process h fn (ShowProof n')
931937 Nothing -> iPrintError "No proof to show"
932938 Just p -> iPrintResult $ showProof False n p
933939
934−process h fn (Prove n')
940+process fn (Prove n')
935941 = do ctxt <- getContext
936942 ist <- getIState
937943 let ns = lookupNames n' ctxt
@@ -949,20 +955,20 @@ process h fn (Prove n')
949955 mapM_ checkDeclTotality (idris_totcheck i)
950956 warnTotality
951957
952−process h fn (HNF t)
958+process fn (HNF t)
953959 = do (tm, ty) <- elabVal recinfo ERHS t
954960 ctxt <- getContext
955961 ist <- getIState
956962 let tm' = hnf ctxt [] tm
957963 iPrintResult (show (delab ist tm'))
958−process h fn (TestInline t)
964+process fn (TestInline t)
959965 = do (tm, ty) <- elabVal recinfo ERHS t
960966 ctxt <- getContext
961967 ist <- getIState
962968 let tm' = inlineTerm ist tm
963969 c <- colourise
964970 iPrintResult (showTm ist (delab ist tm'))
965−process h fn Execute
971+process fn Execute
966972 = idrisCatch
967973 (do ist <- getIState
968974 (m, _) <- elabVal recinfo ERHS
@@ -974,33 +980,33 @@ process h fn Execute
974980 t <- codegen
975981 compile t tmpn m
976982 case idris_outputmode ist of
977− RawOutput -> do runIO $ system tmpn
978− return ()
983+ RawOutput h -> do runIO $ system tmpn
984+ return ()
979985 IdeSlave n h -> runIO . hPutStrLn h $
980986 IdeSlave.convSExp "run-program" tmpn n)
981− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
987+ (\e -> getIState >>= iRenderError . flip pprintErr e)
982988 where fc = fileFC "main"
983−process h fn (Compile codegen f)
989+process fn (Compile codegen f)
984990 = do (m, _) <- elabVal recinfo ERHS
985991 (PApp fc (PRef fc (sUN "run__IO"))
986992 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
987993 compile codegen f m
988994 where fc = fileFC "main"
989−process h fn (LogLvl i) = setLogLevel i
995+process fn (LogLvl i) = setLogLevel i
990996-- Elaborate as if LHS of a pattern (debug command)
991−process h fn (Pattelab t)
997+process fn (Pattelab t)
992998 = do (tm, ty) <- elabVal recinfo ELHS t
993999 iPrintResult $ show tm ++ "\n\n : " ++ show ty
9941000
995−process h fn (Missing n)
1001+process fn (Missing n)
9961002 = do i <- getIState
9971003 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
9981004 case lookupCtxt n (idris_patdefs i) of
999− [] -> ihPrintError h $ "Unknown operator " ++ show n
1005+ [] -> iPrintError $ "Unknown operator " ++ show n
10001006 [(_, tms)] ->
10011007 iPrintResult (showSep "\n" (map (showTm i') tms))
10021008 _ -> iPrintError $ "Ambiguous name"
1003−process h fn (DynamicLink l)
1009+process fn (DynamicLink l)
10041010 = do i <- getIState
10051011 let importdirs = opt_importdirs (idris_options i)
10061012 lib = trim l
@@ -1013,80 +1019,80 @@ process h fn (DynamicLink l)
10131019 return ()
10141020 else putIState $ i { idris_dynamic_libs = x:libs }
10151021 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
1016−process h fn ListDynamic
1022+process fn ListDynamic
10171023 = do i <- getIState
10181024 iputStrLn "Dynamic libraries:"
10191025 showLibs $ idris_dynamic_libs i
10201026 where showLibs [] = return ()
10211027 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
1022−process h fn Metavars
1028+process fn Metavars
10231029 = do ist <- getIState
10241030 let mvs = map fst (idris_metavars ist) \\ primDefs
10251031 case mvs of
10261032 [] -> iPrintError "No global metavariables to solve"
10271033 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
1028−process h fn NOP = return ()
1029−
1030−process h fn (SetOpt ErrContext) = setErrContext True
1031−process h fn (UnsetOpt ErrContext) = setErrContext False
1032−process h fn (SetOpt ShowImpl) = setImpShow True
1033−process h fn (UnsetOpt ShowImpl) = setImpShow False
1034−process h fn (SetOpt ShowOrigErr) = setShowOrigErr True
1035−process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1036−process h fn (SetOpt AutoSolve) = setAutoSolve True
1037−process h fn (UnsetOpt AutoSolve) = setAutoSolve False
1038−process h fn (SetOpt NoBanner) = setNoBanner True
1039−process h fn (UnsetOpt NoBanner) = setNoBanner False
1040−process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
1041−process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1042−
1043−process h fn (SetOpt _) = iPrintError "Not a valid option"
1044−process h fn (UnsetOpt _) = iPrintError "Not a valid option"
1045−process h fn (SetColour ty c) = setColour ty c
1046−process h fn ColourOn
1034+process fn NOP = return ()
1035+
1036+process fn (SetOpt ErrContext) = setErrContext True
1037+process fn (UnsetOpt ErrContext) = setErrContext False
1038+process fn (SetOpt ShowImpl) = setImpShow True
1039+process fn (UnsetOpt ShowImpl) = setImpShow False
1040+process fn (SetOpt ShowOrigErr) = setShowOrigErr True
1041+process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1042+process fn (SetOpt AutoSolve) = setAutoSolve True
1043+process fn (UnsetOpt AutoSolve) = setAutoSolve False
1044+process fn (SetOpt NoBanner) = setNoBanner True
1045+process fn (UnsetOpt NoBanner) = setNoBanner False
1046+process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
1047+process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1048+
1049+process fn (SetOpt _) = iPrintError "Not a valid option"
1050+process fn (UnsetOpt _) = iPrintError "Not a valid option"
1051+process fn (SetColour ty c) = setColour ty c
1052+process fn ColourOn
10471053 = do ist <- getIState
10481054 putIState $ ist { idris_colourRepl = True }
1049−process h fn ColourOff
1055+process fn ColourOff
10501056 = do ist <- getIState
10511057 putIState $ ist { idris_colourRepl = False }
1052−process h fn ListErrorHandlers =
1058+process fn ListErrorHandlers =
10531059 do ist <- getIState
10541060 iPrintResult $ case idris_errorhandlers ist of
10551061 [] -> "No registered error handlers"
10561062 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1057−process h fn (SetConsoleWidth w) = setWidth w
1063+process fn (SetConsoleWidth w) = setWidth w
10581064
1059−process h fn (Apropos a) =
1065+process fn (Apropos a) =
10601066 do ist <- getIState
10611067 let names = apropos ist (T.pack a)
10621068 let aproposInfo = [ (n,
10631069 delabTy ist n,
10641070 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
10651071 | n <- sort names, isUN n ]
1066− ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)
1072+ iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)
10671073 where isUN (UN _) = True
10681074 isUN (NS n _) = isUN n
10691075 isUN _ = False
10701076
1071−process h fn (WhoCalls n) =
1077+process fn (WhoCalls n) =
10721078 do calls <- whoCalls n
10731079 ist <- getIState
1074− ihRenderResult h . vsep $
1080+ iRenderResult . vsep $
10751081 map (\(n, ns) ->
10761082 text "Callers of" <+> prettyName True True [] n <$>
10771083 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
10781084 calls
10791085
1080−process h fn (CallsWho n) =
1086+process fn (CallsWho n) =
10811087 do calls <- callsWho n
10821088 ist <- getIState
1083− ihRenderResult h . vsep $
1089+ iRenderResult . vsep $
10841090 map (\(n, ns) ->
10851091 prettyName True True [] n <+> text "calls:" <$>
10861092 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
10871093 calls
10881094-- IdrisDoc
1089−process h fn (MakeDoc s) =
1095+process fn (MakeDoc s) =
10901096 do istate <- getIState
10911097 let names = words s
10921098 parse n | Success x <- runparser name istate fn n = Right x
@@ -1143,8 +1149,8 @@ idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
11431149 [] -> return ()
11441150
11451151
1146−loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()
1147−loadInputs h inputs toline -- furthest line to read in input source files
1152+loadInputs :: [FilePath] -> Maybe Int -> Idris ()
1153+loadInputs inputs toline -- furthest line to read in input source files
11481154 = idrisCatch
11491155 (do ist <- getIState
11501156 -- if we're in --check and not outputting anything, don't bother
@@ -1196,10 +1202,10 @@ loadInputs h inputs toline -- furthest line to read in input source files
11961202 (\e -> do i <- getIState
11971203 case e of
11981204 At f e' -> do setErrSpan f
1199− ihWarn stdout f $ pprintErr i e'
1205+ iWarn f $ pprintErr i e'
12001206 ProgramLineComment -> return () -- fail elsewhere
12011207 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1202− ihWarn stdout emptyFC $ pprintErr i e)
1208+ iWarn emptyFC $ pprintErr i e)
12031209 where -- load all files, stop if any fail
12041210 tryLoad :: Bool -> [IFileType] -> Idris ()
12051211 tryLoad keepstate [] = warnTotality >> return ()
@@ -1216,7 +1222,7 @@ loadInputs h inputs toline -- furthest line to read in input source files
12161222 then Just l
12171223 else Nothing
12181224 _ -> Nothing
1219− loadFromIFile h f maxline
1225+ loadFromIFile f maxline
12201226 inew <- getIState
12211227 -- FIXME: Save these in IBC to avoid this hack! Need to
12221228 -- preserve it all from source inputs
@@ -1326,9 +1332,9 @@ idrisMain opts =
13261332 addPkgDir "base"
13271333 mapM_ addPkgDir pkgdirs
13281334 elabPrims
1329− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"
1335+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"
13301336 return ()
1331− when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1337+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
13321338 return ()
13331339
13341340 when (runrepl && not idesl) initScript
@@ -1344,14 +1350,14 @@ idrisMain opts =
13441350 iputStrLn banner
13451351
13461352 orig <- getIState
1347− loadInputs stdout inputs Nothing
1353+ loadInputs inputs Nothing
13481354
13491355 runIO $ hSetBuffering stdout LineBuffering
13501356
13511357 ok <- noErrors
13521358 when ok $ case output of
13531359 [] -> return ()
1354− (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1360+ (o:_) -> idrisCatch (process "" (Compile cgn o))
13551361 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
13561362
13571363 case immediate of
@@ -1362,7 +1368,7 @@ idrisMain opts =
13621368 case parseExpr ist str of
13631369 Failure err -> do iputStrLn $ show (fixColour c err)
13641370 runIO $ exitWith (ExitFailure 1)
1365− Success e -> process stdout "" (Eval e))
1371+ Success e -> process "" (Eval e))
13661372 exprs
13671373 runIO $ exitWith ExitSuccess
13681374
@@ -1447,7 +1453,7 @@ initScript = do script <- getInitScript
14471453 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
14481454 Success Proofs -> proofs i
14491455 Success Quit -> iPrintError "Init scripts cannot quit Idris"
1450− Success cmd -> process stdout [] cmd
1456+ Success cmd -> process [] cmd
14511457
14521458getFile :: Opt -> Maybe String
14531459getFile (Filename str) = Just str