Skip to content

Commit

Permalink
Merge pull request idris-lang#1369 from david-christiansen/prover-out…
Browse files Browse the repository at this point in the history
…put-color

Highlight prover output for ideslave
  • Loading branch information
edwinb committed Jul 9, 2014
2 parents f05e088 + e336883 commit f0ba64c
Showing 1 changed file with 5 additions and 3 deletions.
8 changes: 5 additions & 3 deletions src/Idris/Output.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand Down

0 comments on commit f0ba64c

Please sign in to comment.