git.iko.soy/Idris-dev
on master help sign in
Format some messages in the prover
2576d6dJason Felice
src/Idris/Prover.hs+2−2
compare with master
unifiedsplit
@@ -318,7 +318,7 @@ elabloop info fn d prompt prf e prev h env
318 idrisCatch
318 idrisCatch
319 (case cmd of
319 (case cmd of
320 Left err -> do
320 Left err -> do
321− msg <- Left . Msg . show <$> formatMessage err
321+ msg <- fmap (Left . Msg . show) (formatMessage err)
322 return (False, prev, e, False, prf, env, msg)
322 return (False, prev, e, False, prf, env, msg)
323 Right (Left cmd') ->
323 Right (Left cmd') ->
324 case cmd' of
324 case cmd' of
@@ -435,7 +435,7 @@ ploop fn d prompt prf e h
435 (d, st, done, prf', res) <- idrisCatch
435 (d, st, done, prf', res) <- idrisCatch
436 (case cmd of
436 (case cmd of
437 Left err -> do
437 Left err -> do
438− msg <- Left . Msg . show <$> formatMessage err
438+ msg <- fmap (Left . Msg . show) (formatMessage err)
439 return (False, e, False, prf, msg)
439 return (False, e, False, prf, msg)
440 Right Undo -> do (_, st) <- elabStep e loadState
440 Right Undo -> do (_, st) <- elabStep e loadState
441 return (True, st, False, init prf, Right $ iPrintResult "")
441 return (True, st, False, init prf, Right $ iPrintResult "")
src/Idris/REPL.hs−1
@@ -725,7 +725,6 @@ processInput cmd orig inputs efile
725 let opts = idris_options i
725 let opts = idris_options i
726 let quiet = opt_quiet opts
726 let quiet = opt_quiet opts
727 let fn = fromMaybe "" (listToMaybe inputs)
727 let fn = fromMaybe "" (listToMaybe inputs)
728− c <- colourise
729 case parseCmd i "(input)" cmd of
728 case parseCmd i "(input)" cmd of
730 Left err -> Just inputs <$ emit err
729 Left err -> Just inputs <$ emit err
731 Right (Right Reload) ->
730 Right (Right Reload) ->