ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Highlight prover output for ideslave

Browse Source
This commit is contained in:
David Raymond Christiansen 2014-07-09 15:48:13 +02:00
parent 32d47a5304
commit e336883cdf
1 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Idris/Output.hs
View File

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