90bbf06 · Idris-dev · git.iko.soy

libs/base/Debug/Error.idr+1−1

compare with master

unifiedsplit

@@ -8,7 +8,7 @@ import System

8||| @ loc The source location to display for the error

9||| @ message The error to print

10partial

11−error : {default tactics {sourceLocation} loc : SourceLocation} ->

11+error : {default (%runElab sourceLocation) loc : SourceLocation} ->

12 (message : String) ->

13 a

14error {loc = FileLoc filename (line, col) _} message =

libs/base/base.ipkg+1−1

@@ -1,6 +1,6 @@

1package base

2

3−opts = "--nobasepkgs --total -i ../prelude"

3+opts = "--nobasepkgs --total --no-elim-deprecation-warnings -i ../prelude"

4modules = System,

5

6 Debug.Error, Debug.Trace,

libs/prelude/prelude.ipkg+1−1

@@ -1,6 +1,6 @@

1package prelude

2

3−opts = "--nobuiltins --total"

3+opts = "--nobuiltins --total --no-elim-deprecation-warnings"

4modules = Builtins, Prelude, IO,

5

6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

src/Idris/AbsSyntaxTree.hs+1

@@ -503,6 +503,7 @@ data Opt = Filename String

503 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

504 | UseConsoleWidth ConsoleWidth

505 | DumpHighlights

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

506 deriving (Show, Eq)

507 deriving (Show, Eq)

507

508

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

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

src/Idris/CmdOptions.hs+1

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

148

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

151

152

152 where

153 where

153 getExt s = case maybeRead s of

154 getExt s = case maybeRead s of

src/Idris/DeepSeq.hs+2−1

@@ -160,7 +160,8 @@ instance NFData Opt where

160 rnf (AutoWidth) = ()

161 rnf (AutoSolve) = ()

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

163− rnf (DumpHighlights) = ()

163+ rnf DumpHighlights = ()

164+ rnf NoElimDeprecationWarnings = ()

164

165

166

166instance NFData TIData where

167instance NFData TIData where

src/Idris/ParseData.hs+12−2

@@ -157,11 +157,21 @@ DefaultEliminator ::= 'noelim'?

157 -}

158dataOpts :: DataOpts -> IdrisParser DataOpts

159dataOpts opts

160+ = do fc <- reservedFC "%elim"

161+ warnElim fc

160− = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)

162+ dataOpts (DefaultEliminator : DefaultCaseFun : opts)

163+ <|> do fc <- reservedFC "%case"

164+ warnElim fc

161− <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)

165+ dataOpts (DefaultCaseFun : opts)

162 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

166 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

163 <|> return opts

167 <|> return opts

164 <?> "data options"

168 <?> "data options"

169+ where warnElim fc =

170+ do ist <- get

171+ let cmdline = opt_cmdline (idris_options ist)

172+ unless (NoElimDeprecationWarnings `elem` cmdline) $

173+ put ist { parserWarnings =

174+ (fc, Msg "Eliminator generation is deprecated. Use an eliminator generator in a library instead.") : parserWarnings ist }

165

175

166{- | Parses a data type declaration

176{- | Parses a data type declaration

167Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

177Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?