@@ -239,6 +239,12 @@ ideslave orig mods
239239 process stdout fn (CaseSplitAt False line (UN name))
240240 Just (IdeSlave.AddClause line name) ->
241241 process stdout fn (AddClauseFrom False line (UN name))
242+ Just (IdeSlave.AddMissing line name) ->
243+ process stdout fn (AddMissing False line (UN name))
244+ Just (IdeSlave.MakeWithBlock line name) ->
245+ process stdout fn (MakeWith False line (UN name))
246+ Just (IdeSlave.ProofSearch line name hints) ->
247+ process stdout fn (DoProofSearch False line (UN name) (map UN hints))
242248 Nothing -> do iPrintError "did not understand")
243249 (\e -> do iPrintError $ show e)
244250 ideslave orig mods
@@ -567,14 +573,14 @@ process h fn (AddClauseFrom updatefile l n)
567573 cl <- getClause l n fn
568574 -- add clause before first blank line in 'later'
569575 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
570− if updatefile then
571− do let fb = fn ++ "~"
572− runIO $ writeFile fb (unlines (before ++ nonblank)
573− ++ replicate indent ' ' ++
576+ if updatefile
577+ then do let fb = fn ++ "~"
578+ runIO $ writeFile fb (unlines (before ++ nonblank) ++
579+ replicate indent ' ' ++
574580 cl ++ "\n" ++
575− unlines rest)
576− runIO $ copyFile fb fn
577− else ihPrintResult h cl
581+ unlines rest)
582+ runIO $ copyFile fb fn
583+ else ihPrintResult h cl
578584 where
579585 getIndent i n [] = 0
580586 getIndent i n xs | take (length n) xs == n = i
@@ -586,14 +592,14 @@ process h fn (AddProofClauseFrom updatefile l n)
586592 cl <- getProofClause l n fn
587593 -- add clause before first blank line in 'later'
588594 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
589− if updatefile then
590− do let fb = fn ++ "~"
591− runIO $ writeFile fb (unlines (before ++ nonblank)
592− ++ replicate indent ' ' ++
595+ if updatefile
596+ then do let fb = fn ++ "~"
597+ runIO $ writeFile fb (unlines (before ++ nonblank) ++
598+ replicate indent ' ' ++
593599 cl ++ "\n" ++
594− unlines rest)
595− runIO $ copyFile fb fn
596− else ihputStrLn h cl
600+ unlines rest)
601+ runIO $ copyFile fb fn
602+ else ihPrintResult h cl
597603 where
598604 getIndent i n [] = 0
599605 getIndent i n xs | take (length n) xs == n = i
@@ -610,12 +616,12 @@ process h fn (AddMissing updatefile l n)
610616 [] -> return ""
611617 [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms
612618 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
613− if updatefile then
614− do let fb = fn ++ "~"
615− runIO $ writeFile fb (unlines (before ++ nonblank) ++
616− extras ++ unlines rest)
617− runIO $ copyFile fb fn
618− else ihputStrLn h extras
619+ if updatefile
620+ then do let fb = fn ++ "~"
621+ runIO $ writeFile fb (unlines (before ++ nonblank)
622+ ++ extras ++ unlines rest)
623+ runIO $ copyFile fb fn
624+ else ihPrintResult h extras
619625 where showPat = show . stripNS
620626 stripNS tm = mapPT dens tm where
621627 dens (PRef fc n) = PRef fc (nsroot n)
@@ -636,7 +642,7 @@ process h fn (AddMissing updatefile l n)
636642 showPat tm ++ " = ?" ++ nm' ++
637643 "\n" ++ rest)
638644 showNew nm i _ [] = return ""
639−
645+
640646 getIndent i n [] = 0
641647 getIndent i n xs | take (length n) xs == n = i
642648 getIndent i n (x : xs) = getIndent (i + 1) n xs
@@ -653,7 +659,7 @@ process h fn (MakeWith updatefile l n)
653659 ++ with ++ "\n" ++
654660 unlines rest)
655661 runIO $ copyFile fb fn
656− else ihputStrLn h with
662+ else ihPrintResult h with
657663process h fn (DoProofSearch updatefile l n hints)
658664 = do src <- runIO $ readFile fn
659665 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -685,7 +691,7 @@ process h fn (DoProofSearch updatefile l n hints)
685691 updateMeta tyline (show n) newmv ++ "\n"
686692 ++ unlines later)
687693 runIO $ copyFile fb fn
688− else ihputStrLn h newmv
694+ else ihPrintResult h newmv
689695 where dropCtxt 0 sc = sc
690696 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
691697 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc