@@ -77,13 +77,13 @@ elabStep st e = do case runStateT e st of
7777 Error a -> do i <- getIState
7878 fail (pshow i a)
7979
80−dumpState :: IState -> ProofState -> IO ()
80+dumpState :: IState -> ProofState -> Idris ()
8181dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
82− putStrLn . render $ pretty nm <> colon <+> text "No more goals."
82+ iputGoal . render $ pretty nm <> colon <+> text "No more goals."
8383dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
8484 let OK ty = goalAtFocus ps
8585 let OK env = envAtFocus ps
86− putStrLn . render $
86+ iputGoal . render $
8787 prettyOtherGoals hs $$
8888 prettyAssumptions env $$
8989 prettyGoal ty
@@ -127,15 +127,19 @@ lifte st e = do (v, _) <- elabStep st e
127127ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
128128ploop d prompt prf e h
129129 = do i <- getIState
130− when d $ liftIO $ dumpState i (proof e)
131− (x, h') <- runInputT (proverSettings e) $
132− -- Manually track the history so that we can use the proof state
133− do _ <- case h of
134− Just history -> putHistory history
135− Nothing -> return ()
136− l <- getInputLine (prompt ++ "> ")
137− h' <- getHistory
138− return (l, Just h')
130+ when d $ dumpState i (proof e)
131+ (x, h') <-
132+ case idris_outputmode i of
133+ RawOutput -> runInputT (proverSettings e) $
134+ -- Manually track the history so that we can use the proof state
135+ do _ <- case h of
136+ Just history -> putHistory history
137+ Nothing -> return ()
138+ l <- getInputLine (prompt ++ "> ")
139+ h' <- getHistory
140+ return (l, Just h')
141+ IdeSlave n -> -- setprompt -- waitforinput
142+ return (Just "trivial", h)
139143 (cmd, step) <- case x of
140144 Nothing -> fail "Abandoned"
141145 Just input -> do return (parseTac i input, input)