@@ -17,7 +17,7 @@ import Idris.UnusedArgs
1717import Idris.Docs
1818import Idris.Help
1919import Idris.Completion
20−import Idris.IdeSlave
20+import qualified Idris.IdeSlave as IdeSlave
2121import Idris.Chaser
2222import Idris.Imports
2323import Idris.Colours
@@ -194,17 +194,17 @@ ideslave :: IState -> [FilePath] -> Idris ()
194194ideslave orig mods
195195 = do idrisCatch
196196 (do l <- runIO $ getLine
197− (sexp, id) <- case parseMessage l of
197+ (sexp, id) <- case IdeSlave.parseMessage l of
198198 Left err -> ierror err
199199 Right (sexp, id) -> return (sexp, id)
200200 i <- getIState
201201 putIState $ i { idris_outputmode = (IdeSlave id) }
202− case sexpToCommand sexp of
203− Just (Interpret cmd) ->
204− do let fn = case mods of
205− (f:_) -> f
206− _ -> ""
207− c <- colourise
202+ let fn = case mods of
203+ (f:_) -> f
204+ _ -> ""
205+ case IdeSlave.sexpToCommand sexp of
206+ Just (IdeSlave.Interpret cmd) ->
207+ do c <- colourise
208208 case parseCmd i "(input)" cmd of
209209 Failure err -> iPrintError $ show (fixColour c err)
210210 Success (Prove n') -> do iPrintResult ""
@@ -215,11 +215,11 @@ ideslave orig mods
215215 Success cmd -> idrisCatch
216216 (ideslaveProcess fn cmd)
217217 (\e -> getIState >>= iPrintError . flip pshow e)
218− Just (REPLCompletions str) ->
218+ Just (IdeSlave.REPLCompletions str) ->
219219 do (unused, compls) <- replCompletion (reverse str, "")
220− let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
221− runIO $ putStrLn $ convSExp "return" good id
222− Just (LoadFile filename) ->
220+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]
221+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id
222+ Just (IdeSlave.LoadFile filename) ->
223223 do clearErr
224224 putIState (orig { idris_options = idris_options i,
225225 idris_outputmode = (IdeSlave id) })
@@ -233,6 +233,20 @@ ideslave orig mods
233233 Nothing -> iPrintResult $ "loaded " ++ filename
234234 Just x -> iPrintError $ "didn't load " ++ filename
235235 ideslave orig [filename]
236+ Just (IdeSlave.TypeOf name) ->
237+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))
238+ Just (IdeSlave.CaseSplit line name) ->
239+ process stdout fn (CaseSplitAt False line (UN name))
240+ Just (IdeSlave.AddClause line name) ->
241+ process stdout fn (AddClauseFrom False line (UN name))
242+ Just (IdeSlave.AddProofClause line name) ->
243+ process stdout fn (AddProofClauseFrom False line (UN name))
244+ Just (IdeSlave.AddMissing line name) ->
245+ process stdout fn (AddMissing False line (UN name))
246+ Just (IdeSlave.MakeWithBlock line name) ->
247+ process stdout fn (MakeWith False line (UN name))
248+ Just (IdeSlave.ProofSearch line name hints) ->
249+ process stdout fn (DoProofSearch False line (UN name) (map UN hints))
236250 Nothing -> do iPrintError "did not understand")
237251 (\e -> do iPrintError $ show e)
238252 ideslave orig mods
@@ -435,10 +449,10 @@ process h fn (Check (PRef _ n))
435449 case lookupNames n ctxt of
436450 ts@(t:_) ->
437451 case lookup t (idris_metavars ist) of
438− Just (_, i) -> showMetavarInfo c imp ist n i
439− Nothing -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++
440− showImp (Just ist) imp c (delabTy ist n)) ts
441− ihPrintResult h ""
452+ Just (_, i) -> ihPrintResult h (showMetavarInfo c imp ist n i)
453+ Nothing -> ihPrintResult h $
454+ concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++
455+ showImp (Just ist) imp c (delabTy ist n)) $ ts
442456 [] -> ihPrintError h $ "No such variable " ++ show n
443457 where
444458 showMetavarInfo c imp ist n i
@@ -446,18 +460,19 @@ process h fn (Check (PRef _ n))
446460 (ty:_) -> putTy c imp ist i (delab ist ty)
447461 putTy c imp ist 0 sc = putGoal c imp ist sc
448462 putTy c imp ist i (PPi _ n t sc)
449− = do ihputStrLn h $ " " ++
450− (case n of
451− MN _ _ -> "_"
452− UN ('_':'_':_) -> "_"
453− _ -> showName (Just ist) [] False c n) ++
454− " : " ++ showImp (Just ist) imp c t
455− putTy c imp ist (i-1) sc
463+ = let current = " " ++
464+ (case n of
465+ MN _ _ -> "_"
466+ UN ('_':'_':_) -> "_"
467+ _ -> showName (Just ist) [] False c n) ++
468+ " : " ++ showImp (Just ist) imp c t ++ "\n"
469+ in
470+ current ++ putTy c imp ist (i-1) sc
456471 putTy c imp ist _ sc = putGoal c imp ist sc
457472 putGoal c imp ist g
458− = do ihputStrLn h $ "--------------------------------------"
459− ihputStrLn h $ showName (Just ist) [] False c n ++ " : "
460− ++ showImp (Just ist) imp c g
473+ = "--------------------------------------\n" ++
474+ showName (Just ist) [] False c n ++ " : " ++
475+ showImp (Just ist) imp c g
461476
462477
463478process h fn (Check t)
@@ -470,7 +485,7 @@ process h fn (Check t)
470485 case tm of
471486 TType _ -> ihPrintResult h ("Type : Type 1")
472487 _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
473− showImp (Just ist) imp c (delab ist ty))
488+ showImp (Just ist) imp c (delab ist ty))
474489
475490process h fn (DocStr n)
476491 = do i <- getIState
@@ -544,12 +559,12 @@ process h fn (CaseSplitAt updatefile l n)
544559 let (before, (ap : later)) = splitAt (l-1) (lines src)
545560 res' <- replaceSplits ap res
546561 let new = concat res'
547− if updatefile then
548− do let fb = fn ++ "~" -- make a backup!
549− runIO $ writeFile fb (unlines before ++ new ++ unlines later)
550− runIO $ copyFile fb fn
551− else -- do ihputStrLn h (show res)
552− ihputStrLn h new
562+ if updatefile
563+ then do let fb = fn ++ "~" -- make a backup!
564+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)
565+ runIO $ copyFile fb fn
566+ else -- do ihputStrLn h (show res)
567+ ihPrintResult h new
553568process h fn (AddClauseFrom updatefile l n)
554569 = do src <- runIO $ readFile fn
555570 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -557,14 +572,14 @@ process h fn (AddClauseFrom updatefile l n)
557572 cl <- getClause l n fn
558573 -- add clause before first blank line in 'later'
559574 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
560− if updatefile then
561− do let fb = fn ++ "~"
562− runIO $ writeFile fb (unlines (before ++ nonblank)
563− ++ replicate indent ' ' ++
575+ if updatefile
576+ then do let fb = fn ++ "~"
577+ runIO $ writeFile fb (unlines (before ++ nonblank) ++
578+ replicate indent ' ' ++
564579 cl ++ "\n" ++
565− unlines rest)
566− runIO $ copyFile fb fn
567− else ihputStrLn h cl
580+ unlines rest)
581+ runIO $ copyFile fb fn
582+ else ihPrintResult h cl
568583 where
569584 getIndent i n [] = 0
570585 getIndent i n xs | take (length n) xs == n = i
@@ -576,14 +591,14 @@ process h fn (AddProofClauseFrom updatefile l n)
576591 cl <- getProofClause l n fn
577592 -- add clause before first blank line in 'later'
578593 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
579− if updatefile then
580− do let fb = fn ++ "~"
581− runIO $ writeFile fb (unlines (before ++ nonblank)
582− ++ replicate indent ' ' ++
594+ if updatefile
595+ then do let fb = fn ++ "~"
596+ runIO $ writeFile fb (unlines (before ++ nonblank) ++
597+ replicate indent ' ' ++
583598 cl ++ "\n" ++
584− unlines rest)
585− runIO $ copyFile fb fn
586− else ihputStrLn h cl
599+ unlines rest)
600+ runIO $ copyFile fb fn
601+ else ihPrintResult h cl
587602 where
588603 getIndent i n [] = 0
589604 getIndent i n xs | take (length n) xs == n = i
@@ -600,12 +615,12 @@ process h fn (AddMissing updatefile l n)
600615 [] -> return ""
601616 [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms
602617 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
603− if updatefile then
604− do let fb = fn ++ "~"
605− runIO $ writeFile fb (unlines (before ++ nonblank) ++
606− extras ++ unlines rest)
607− runIO $ copyFile fb fn
608− else ihputStrLn h extras
618+ if updatefile
619+ then do let fb = fn ++ "~"
620+ runIO $ writeFile fb (unlines (before ++ nonblank)
621+ ++ extras ++ unlines rest)
622+ runIO $ copyFile fb fn
623+ else ihPrintResult h extras
609624 where showPat = show . stripNS
610625 stripNS tm = mapPT dens tm where
611626 dens (PRef fc n) = PRef fc (nsroot n)
@@ -626,7 +641,7 @@ process h fn (AddMissing updatefile l n)
626641 showPat tm ++ " = ?" ++ nm' ++
627642 "\n" ++ rest)
628643 showNew nm i _ [] = return ""
629−
644+
630645 getIndent i n [] = 0
631646 getIndent i n xs | take (length n) xs == n = i
632647 getIndent i n (x : xs) = getIndent (i + 1) n xs
@@ -643,7 +658,7 @@ process h fn (MakeWith updatefile l n)
643658 ++ with ++ "\n" ++
644659 unlines rest)
645660 runIO $ copyFile fb fn
646− else ihputStrLn h with
661+ else ihPrintResult h with
647662process h fn (DoProofSearch updatefile l n hints)
648663 = do src <- runIO $ readFile fn
649664 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -675,7 +690,7 @@ process h fn (DoProofSearch updatefile l n hints)
675690 updateMeta tyline (show n) newmv ++ "\n"
676691 ++ unlines later)
677692 runIO $ copyFile fb fn
678− else ihputStrLn h newmv
693+ else ihPrintResult h newmv
679694 where dropCtxt 0 sc = sc
680695 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
681696 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc