e39254c · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

@@ -487,7 +487,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

487 | ProofState | ProofTerm | Undo

488 | Try (PTactic' t) (PTactic' t)

489 | TSeq (PTactic' t) (PTactic' t)

490− | Qed

490+ | Qed | Abandon

491 deriving (Show, Eq, Functor)

492{-!

493deriving instance Binary PTactic'

src/Idris/Parser.hs+2

@@ -1184,6 +1184,8 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1184 <|> do reserved "term"; return ProofTerm

1185 <|> do reserved "undo"; return Undo

1186 <|> do reserved "qed"; return Qed

1187+ <|> do reserved "abandon"; return Abandon

1188+ <|> do lchar ':'; reserved "q"; return Abandon

1187 where

1189 where

1188 imp = do lchar '?'; return False

1190 imp = do lchar '?'; return False

1189 <|> do lchar '_'; return True

1191 <|> do lchar '_'; return True

src/Idris/Prover.hs+3

@@ -93,6 +93,9 @@ ploop d prompt prf e

93 (cmd, step) <- case x of

94 Nothing -> fail "Abandoned"

95 Just input -> do return (parseTac i input, input)

96+ case cmd of

97+ Right Abandon -> fail "Abandoned"

98+ _ -> return ()

96 (d, st, done, prf') <- idrisCatch

99 (d, st, done, prf') <- idrisCatch

97 (case cmd of

100 (case cmd of

98 Left err -> do iputStrLn (show err)

101 Left err -> do iputStrLn (show err)