ed0f118 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1195 from ziman/set-warnreach

Add :set warnreach + usage check after every :r

commited0f11886e5e84bbbdf4ff0bd44c8255b0486bb7 authorEdwin Brady <edwin.brady@gmail.com> dateMon 5 May 2014, 11:25 (12 years ago) parent67517aa 10509f6

3 files changed+21−5

compare with master

unifiedsplit

src/Idris/ASTUtils.hs+9 src/Idris/REPL.hs+11−5 src/Idris/REPLParser.hs+1

src/Idris/ASTUtils.hs+9

@@ -123,3 +123,12 @@ ist_callgraph n =

123123-- some fields of the CGInfo record

124124cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

125125cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

126+

127+

128+-- Commandline flags

129+--------------------

130+

131+opts_idrisCmdline :: Field IState [Opt]

132+opts_idrisCmdline =

133+ Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })

134+ . Field idris_options (\v ist -> ist{ idris_options = v })

src/Idris/REPL.hs+11−5

@@ -4,6 +4,7 @@

44module Idris.REPL where

66import Idris.AbsSyntax

7+import Idris.ASTUtils

78import Idris.Apropos (apropos)

89import Idris.REPLParser

910import Idris.ElabDecls

@@ -1032,6 +1033,8 @@ process h fn (SetOpt AutoSolve) = setAutoSolve True

10321033process h fn (UnsetOpt AutoSolve) = setAutoSolve False

10331034process h fn (SetOpt NoBanner) = setNoBanner True

10341035process h fn (UnsetOpt NoBanner) = setNoBanner False

1036+process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1037+process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

10351038

10361039process h fn (SetOpt _) = iPrintError "Not a valid option"

10371040process h fn (UnsetOpt _) = iPrintError "Not a valid option"

@@ -1255,7 +1258,13 @@ loadInputs h inputs

12551258 _ -> return ()

12561259 ist <- getIState

12571260 putIState (ist { idris_tyinfodata = tidata,

1258− idris_patdefs = patdefs }))

1261+ idris_patdefs = patdefs })

1262+

1263+ case opt getOutput opts of

1264+ [] -> performUsageAnalysis -- interactive

1265+ _ -> return [] -- batch, will be checked by the compiler

1266+

1267+ return ())

12591268 (\e -> do i <- getIState

12601269 case e of

12611270 At f e' -> do setErrSpan f

@@ -1399,10 +1408,7 @@ idrisMain opts =

13991408

14001409 ok <- noErrors

14011410 when ok $ case output of

1402− -- just do the checks

1403− [] -> performUsageAnalysis >> return ()

1404−

1405− -- the compiler will run usage analysis itself

1411+ [] -> return ()

14061412 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

14071413 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

14081414

src/Idris/REPLParser.hs+1

@@ -120,6 +120,7 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext

120120 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

121121 <|> do discard (P.symbol "autosolve"); return AutoSolve

122122 <|> do discard (P.symbol "nobanner") ; return NoBanner

123+ <|> do discard (P.symbol "warnreach"); return WarnReach

123124

124125codegenOption :: P.IdrisParser Codegen

125126codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript