git.iko.soy/Idris-dev
on master help sign in
Fixed issue #3883

Seven missing patterns for the process function (src/Idris/REPL.hs) were added. This makes patterns in the function exhaustive.

commit6ea3989ac664fe07717676e317d12efeea735001 authorMarko Dimjašević <marko@cs.utah.edu> dateTue 5 Sep 2017, 23:14 (9 years ago) parentf925538
1 file changed+11
compare with master
unifiedsplit
src/Idris/REPL.hs+11
src/Idris/REPL.hs+11
@@ -1474,6 +1474,17 @@ process fn (PPrint fmt width t)
14741474 ty' = normaliseC ctxt [] ty
14751475 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
14761476
1477+
1478+process fn Quit = iPrintError "Unimplemented pattern for command Quit"
1479+process fn Reload = iPrintError "Unimplemented pattern for command Reload"
1480+process fn Watch = iPrintError "Unimplemented pattern for command Watch"
1481+process fn (Load _ _) = iPrintError "Unimplemented pattern for command Load"
1482+process fn Edit = iPrintError "Unimplemented pattern for command Edit"
1483+process fn Proofs = iPrintError "Unimplemented pattern for command Proofs"
1484+process fn (Verbosity _)
1485+ = iPrintError "Unimplemented pattern for command Verbosity"
1486+
1487+
14771488showTotal :: Totality -> IState -> Doc OutputAnnotation
14781489showTotal t@(Partial (Other ns)) i
14791490 = text "possibly not total due to:" <$>