e36c883 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix #1015

Issuing 'undo' in the prover when there is nothing to undo should result in a less scary looking error message.

commite36c88320e0be93e7ecffad496f34132b2a15386 authorraichoo <raichoo@googlemail.com> dateThu 1 May 2014, 11:58 (12 years ago) parentf9827ac

2 files changed+2−2

unifiedsplit

src/Idris/Core/Elaborate.hs+1−1

@@ -64,7 +64,7 @@ loadState :: Elab' aux ()

6464loadState = do (ES p s e) <- get

6565 case e of

6666 Just st -> put st

67− _ -> fail "Nothing to undo"

67+ _ -> lift $ Error . Msg $ "Nothing to undo"

6868

6969getNameFrom :: Name -> Elab' aux Name

7070getNameFrom n = do (ES (p, a) s e) <- get

src/Idris/Core/ProofState.hs+1−1

@@ -872,7 +872,7 @@ processTactic QED ps = case holes ps of

872872 _ -> fail "Still holes to fill."

873873processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

874874processTactic Undo ps = case previous ps of

875− Nothing -> fail "Nothing to undo."

875+ Nothing -> Error . Msg $ "Nothing to undo."

876876 Just pold -> return (pold, "")

877877processTactic EndUnify ps

878878 = let (h, ns_in) = unified ps