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