git.iko.soy/Idris-dev
on master help sign in
Make it possible to disable tactic deprecation
commit1d40dbd962118ed36b3aaea5fa2c9ac3be977030 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 19 Sep 2015, 14:20 (11 years ago) parent6cf7f5a
5 files changed+17−8
compare with master
unifiedsplit
CHANGELOG+3−1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/CmdOptions.hs+1 src/Idris/DeepSeq.hs+1 src/Idris/ParseExpr.hs+10−6
CHANGELOG+3−1
@@ -31,8 +31,10 @@ Tool updates
3131
3232Miscellaneous updates
3333---------------------
34+* Disable the deprecation warnings for %elim and old-style tactic scripts
35+ with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings
36+ flags.
3437
35−[None so far]
3638
3739New in 0.9.19:
3840--------------
src/Idris/AbsSyntaxTree.hs+2−1
@@ -500,10 +500,11 @@ data Opt = Filename String
500500 | Client String
501501 | ShowOrigErr
502502 | AutoWidth -- ^ Automatically adjust terminal width
503− | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
503+ | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
504504 | UseConsoleWidth ConsoleWidth
505505 | DumpHighlights
506506 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
507+ | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
507508 deriving (Show, Eq)
508509
509510data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
src/Idris/CmdOptions.hs+1
@@ -149,6 +149,7 @@ parseFlags = many $
149149 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))
150150 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")
151151 <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")
152+ <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")
152153
153154 where
154155 getExt s = case maybeRead s of
src/Idris/DeepSeq.hs+1
@@ -162,6 +162,7 @@ instance NFData Opt where
162162 rnf (UseConsoleWidth cw) = rnf cw `seq` ()
163163 rnf DumpHighlights = ()
164164 rnf NoElimDeprecationWarnings = ()
165+ rnf NoOldTacticDeprecationWarnings = ()
165166
166167
167168instance NFData TIData where
src/Idris/ParseExpr.hs+10−6
@@ -331,6 +331,14 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })
331331 return (lhs, r)
332332 <?> "case option"
333333
334+warnTacticDeprecation :: FC -> IdrisParser ()
335+warnTacticDeprecation fc =
336+ do ist <- get
337+ let cmdline = opt_cmdline (idris_options ist)
338+ unless (NoOldTacticDeprecationWarnings `elem` cmdline) $
339+ put ist { parserWarnings =
340+ (fc, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }
341+
334342{- | Parses a proof block
335343@
336344ProofExpr ::=
@@ -342,9 +350,7 @@ proofExpr :: SyntaxInfo -> IdrisParser PTerm
342350proofExpr syn = do kw <- reservedFC "proof"
343351 ts <- indentedBlock1 (tactic syn)
344352 highlightP kw AnnKeyword
345− ist <- get
346− put ist { parserWarnings =
347− (kw, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }
353+ warnTacticDeprecation kw
348354 return $ PProof ts
349355 <?> "proof block"
350356
@@ -359,9 +365,7 @@ tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
359365tacticsExpr syn = do kw <- reservedFC "tactics"
360366 ts <- indentedBlock1 (tactic syn)
361367 highlightP kw AnnKeyword
362− ist <- get
363− put ist { parserWarnings =
364− (kw, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }
368+ warnTacticDeprecation kw
365369 return $ PTactics ts
366370 <?> "tactics block"
367371