7a2acb1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use formatMessage instead of parseErrorDoc

commit7a2acb1133fe97ae6a3b097b437d4a159e7bf747 authorJason Felice <jason.m.felice@gmail.com> dateTue 12 Dec 2017, 12:01 (9 years ago) parent74ddf72

3 files changed+8−5

compare with master

unifiedsplit

src/Idris/Output.hs+1−1 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+6−3

src/Idris/Output.hs+1−1

@@ -9,7 +9,7 @@ Maintainer : The Idris Community.

99{-# LANGUAGE FlexibleInstances #-}

1010{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1111

12−module Idris.Output (clearHighlights, emit, idemodePutSExp, iPrintError, iPrintFunTypes,

12+module Idris.Output (clearHighlights, emit, formatMessage, idemodePutSExp, iPrintError, iPrintFunTypes,

1313 iPrintResult, iPrintTermWithType, iputGoal, iputStr, iputStrLn,

1414 iRender, iRenderError, iRenderOutput, iRenderResult, iWarn,

1515 prettyDocumentedIst, printUndefinedNames, pshow, renderExternal,

src/Idris/Parser.hs+1−1

@@ -1472,7 +1472,7 @@ parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [Im

14721472parseImports fname input

14731473 = do i <- getIState

14741474 case runparser imports i fname input of

1475− Left err -> ifail . show . parseErrorDoc $ err

1475+ Left err -> formatMessage err >>= ifail . show

14761476 Right (x, annots, i) ->

14771477 do putIState i

14781478 fname' <- runIO $ Dir.makeAbsolute fname

src/Idris/Prover.hs+6−3

@@ -317,8 +317,9 @@ elabloop info fn d prompt prf e prev h env

317317 (d, prev', st, done, prf', env', res) <-

318318 idrisCatch

319319 (case cmd of

320− Left err ->

321− return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)

320+ Left err -> do

321+ msg <- Left . Msg . show <$> formatMessage err

322+ return (False, prev, e, False, prf, env, msg)

322323 Right (Left cmd') ->

323324 case cmd' of

324325 EQED -> do hs <- lifte e get_holes

@@ -433,7 +434,9 @@ ploop fn d prompt prf e h

433434 _ -> return ()

434435 (d, st, done, prf', res) <- idrisCatch

435436 (case cmd of

436− Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

437+ Left err -> do

438+ msg <- Left . Msg . show <$> formatMessage err

439+ return (False, e, False, prf, msg)

437440 Right Undo -> do (_, st) <- elabStep e loadState

438441 return (True, st, False, init prf, Right $ iPrintResult "")

439442 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")