1d40dbd · Idris-dev · git.iko.soy

CHANGELOG+3−1

compare with master

unifiedsplit

@@ -31,8 +31,10 @@ Tool updates

31

32Miscellaneous updates

33---------------------

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.

34

37

35−[None so far]

36

38

37New in 0.9.19:

39New in 0.9.19:

38--------------

40--------------

src/Idris/AbsSyntaxTree.hs+2−1

@@ -500,10 +500,11 @@ data Opt = Filename String

500 | Client String

501 | ShowOrigErr

502 | 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

504 | UseConsoleWidth ConsoleWidth

505 | DumpHighlights

506 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

507+ | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

507 deriving (Show, Eq)

508 deriving (Show, Eq)

508

509

509data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

510data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

src/Idris/CmdOptions.hs+1

@@ -149,6 +149,7 @@ parseFlags = many $

149 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

150 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

151 <|> 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")

152

153

153 where

154 where

154 getExt s = case maybeRead s of

155 getExt s = case maybeRead s of

src/Idris/DeepSeq.hs+1

@@ -162,6 +162,7 @@ instance NFData Opt where

162 rnf (UseConsoleWidth cw) = rnf cw `seq` ()

163 rnf DumpHighlights = ()

164 rnf NoElimDeprecationWarnings = ()

165+ rnf NoOldTacticDeprecationWarnings = ()

165

166

167

167instance NFData TIData where

168instance NFData TIData where

src/Idris/ParseExpr.hs+10−6

@@ -331,6 +331,14 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })

331 return (lhs, r)

332 <?> "case option"

333

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+

334{- | Parses a proof block

342{- | Parses a proof block

335@

343@

336ProofExpr ::=

344ProofExpr ::=

@@ -342,9 +350,7 @@ proofExpr :: SyntaxInfo -> IdrisParser PTerm

342proofExpr syn = do kw <- reservedFC "proof"

350proofExpr syn = do kw <- reservedFC "proof"

343 ts <- indentedBlock1 (tactic syn)

351 ts <- indentedBlock1 (tactic syn)

344 highlightP kw AnnKeyword

352 highlightP kw AnnKeyword

345− ist <- get

353+ warnTacticDeprecation kw

346− put ist { parserWarnings =

347− (kw, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }

348 return $ PProof ts

354 return $ PProof ts

349 <?> "proof block"

355 <?> "proof block"

350

356

@@ -359,9 +365,7 @@ tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

359tacticsExpr syn = do kw <- reservedFC "tactics"

365tacticsExpr syn = do kw <- reservedFC "tactics"

360 ts <- indentedBlock1 (tactic syn)

366 ts <- indentedBlock1 (tactic syn)

361 highlightP kw AnnKeyword

367 highlightP kw AnnKeyword

362− ist <- get

368+ warnTacticDeprecation kw

363− put ist { parserWarnings =

364− (kw, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }

365 return $ PTactics ts

369 return $ PTactics ts

366 <?> "tactics block"

370 <?> "tactics block"

367

371