36527f6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Report REPL errors in IDESlave with highlighting

commit36527f6e5f01814c1565e744442be764d35389b5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 12 Feb 2014, 22:24 (13 years ago) parent57af985

2 files changed+15−2

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+13 src/Idris/REPL.hs+2−2

src/Idris/AbsSyntax.hs+13

@@ -579,6 +579,19 @@ fancifyAnnots _ annot = annot

579579type1Doc :: Doc OutputAnnotation

580580type1Doc = (annotate AnnConstType $ text "Type 1")

581581

582+-- | Show an error with semantic highlighting

583+ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

584+ihRenderError h e = do ist <- getIState

585+ case idris_outputmode ist of

586+ RawOutput -> consoleDisplayAnnotated h e

587+ IdeSlave n -> do

588+ (str, spans) <- fmap displaySpans .

589+ iRender .

590+ fmap (fancifyAnnots ist) $

591+ e

592+ let good = [SymbolAtom "error", toSExp str, toSExp spans]

593+ runIO . hPutStrLn h $ convSExp "return" good n

594+

582595ihPrintError :: Handle -> String -> Idris ()

583596ihPrintError h s = do i <- getIState

584597 case idris_outputmode i of

src/Idris/REPL.hs+2−2

@@ -227,11 +227,11 @@ ideslave orig mods

227227 Success (Prove n') -> do iPrintResult ""

228228 idrisCatch

229229 (process stdout fn (Prove n'))

230− (\e -> getIState >>= iPrintError . flip pshow e)

230+ (\e -> getIState >>= ihRenderError . flip pprintErr e)

231231 isetPrompt (mkPrompt mods)

232232 Success cmd -> idrisCatch

233233 (ideslaveProcess fn cmd)

234− (\e -> getIState >>= iPrintError . flip pshow e)

234+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

235235 Just (IdeSlave.REPLCompletions str) ->

236236 do (unused, compls) <- replCompletion (reverse str, "")

237237 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]