@@ -141,13 +141,15 @@ ideslavePutSExp cmd info = do i <- getIState
141 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
141 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
142 _ -> return ()
142 _ -> return ()
144−-- this needs some typing magic and more structured output towards emacs
144+-- TODO: send structured output similar to the metavariable list
145iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
145iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
146iputGoal g = do i <- getIState
146iputGoal g = do i <- getIState
147 case idris_outputmode i of
147 case idris_outputmode i of
148 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
148 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
149− IdeSlave n -> runIO . putStrLn $
149+ IdeSlave n ->
150+ let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g
151+ goal = [toSExp str, toSExp spans]
150− convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
152+ in runIO . putStrLn $ convSExp "write-goal" goal n
152-- | Warn about totality problems without failing to compile
154-- | Warn about totality problems without failing to compile
153warnTotality :: Idris ()
155warnTotality :: Idris ()