git.iko.soy/Idris-dev
on master help sign in
define and use iputGoal instead of putStrLn
d7c8e63Hannes Mehnert
src/Idris/AbsSyntax.hs+7
compare with master
unifiedsplit
@@ -279,6 +279,13 @@ iputStrLn s = do i <- getIState
279 _ -> write
279 _ -> write
280 where write = liftIO $ putStrLn $ convSExp "write-string" s n
280 where write = liftIO $ putStrLn $ convSExp "write-string" s n
281
281
282+-- this needs some typing magic and more structured output towards emacs
283+iputGoal :: String -> Idris ()
284+iputGoal s = do i <- getIState
285+ case idris_outputmode i of
286+ RawOutput -> liftIO $ putStrLn s
287+ IdeSlave n -> liftIO $ putStrLn $ convSExp "write-goal" s n
288+
282iWarn :: FC -> String -> Idris ()
289iWarn :: FC -> String -> Idris ()
283iWarn fc err = do i <- getIState
290iWarn fc err = do i <- getIState
284 case idris_outputmode i of
291 case idris_outputmode i of
src/Idris/Prover.hs+16−12
@@ -77,13 +77,13 @@ elabStep st e = do case runStateT e st of
77 Error a -> do i <- getIState
77 Error a -> do i <- getIState
78 fail (pshow i a)
78 fail (pshow i a)
79
79
80−dumpState :: IState -> ProofState -> IO ()
80+dumpState :: IState -> ProofState -> Idris ()
81dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
81dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
82− putStrLn . render $ pretty nm <> colon <+> text "No more goals."
82+ iputGoal . render $ pretty nm <> colon <+> text "No more goals."
83dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
83dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
84 let OK ty = goalAtFocus ps
84 let OK ty = goalAtFocus ps
85 let OK env = envAtFocus ps
85 let OK env = envAtFocus ps
86− putStrLn . render $
86+ iputGoal . render $
87 prettyOtherGoals hs $$
87 prettyOtherGoals hs $$
88 prettyAssumptions env $$
88 prettyAssumptions env $$
89 prettyGoal ty
89 prettyGoal ty
@@ -127,15 +127,19 @@ lifte st e = do (v, _) <- elabStep st e
127ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
127ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
128ploop d prompt prf e h
128ploop d prompt prf e h
129 = do i <- getIState
129 = do i <- getIState
130− when d $ liftIO $ dumpState i (proof e)
130+ when d $ dumpState i (proof e)
131+ (x, h') <-
132+ case idris_outputmode i of
131− (x, h') <- runInputT (proverSettings e) $
133+ RawOutput -> runInputT (proverSettings e) $
132− -- Manually track the history so that we can use the proof state
134+ -- Manually track the history so that we can use the proof state
133− do _ <- case h of
135+ do _ <- case h of
134− Just history -> putHistory history
136+ Just history -> putHistory history
135− Nothing -> return ()
137+ Nothing -> return ()
136− l <- getInputLine (prompt ++ "> ")
138+ l <- getInputLine (prompt ++ "> ")
137− h' <- getHistory
139+ h' <- getHistory
138− return (l, Just h')
140+ return (l, Just h')
141+ IdeSlave n -> -- setprompt -- waitforinput
142+ return (Just "trivial", h)
139 (cmd, step) <- case x of
143 (cmd, step) <- case x of
140 Nothing -> fail "Abandoned"
144 Nothing -> fail "Abandoned"
141 Just input -> do return (parseTac i input, input)
145 Just input -> do return (parseTac i input, input)