22587b2 · Idris-dev · git.iko.soy

src/Idris/Main.hs+4−3

compare with master

unifiedsplit

@@ -25,6 +25,7 @@ import Idris.ModeCommon

25import Idris.Options

26import Idris.Output

27import Idris.Parser hiding (indent)

28+import Idris.Parser.Helpers (parseErrorDoc)

28import Idris.REPL

29import Idris.REPL

29import Idris.REPL.Commands

30import Idris.REPL.Commands

30import Idris.REPL.Parser

31import Idris.REPL.Parser

@@ -195,7 +196,7 @@ idrisMain opts =

195 mapM_ (\str -> do ist <- getIState

196 mapM_ (\str -> do ist <- getIState

196 c <- colourise

197 c <- colourise

197 case parseExpr ist str of

198 case parseExpr ist str of

198− Left err -> do iputStrLn $ show (fixColour c err)

199+ Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

199 runIO $ exitWith (ExitFailure 1)

200 runIO $ exitWith (ExitFailure 1)

200 Right e -> process "" (Eval e))

201 Right e -> process "" (Eval e))

201 exprs

202 exprs

@@ -272,7 +273,7 @@ execScript :: String -> Idris ()

272execScript expr = do i <- getIState

273execScript expr = do i <- getIState

273 c <- colourise

274 c <- colourise

274 case parseExpr i expr of

275 case parseExpr i expr of

275− Left err -> do iputStrLn $ show (fixColour c err)

276+ Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

276 runIO $ exitWith (ExitFailure 1)

277 runIO $ exitWith (ExitFailure 1)

277 Right term -> do ctxt <- getContext

278 Right term -> do ctxt <- getContext

278 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

279 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

@@ -299,7 +300,7 @@ initScript = do script <- runIO $ getIdrisInitScript

299 runInit h

300 runInit h

300 processLine i cmd input clr =

301 processLine i cmd input clr =

301 case parseCmd i input cmd of

302 case parseCmd i input cmd of

302− Left err -> runIO $ print (fixColour clr err)

303+ Left err -> runIO . print . fixColour clr . parseErrorDoc $ err

303 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"

304 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"

304 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

305 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

305 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

306 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

src/Idris/Package/Parser.hs+1−1

@@ -56,7 +56,7 @@ parseDesc fp = do

56 then do

57 p <- readFile fp

58 case runparser pPkg defaultPkg fp p of

59− Left err -> fail (show $ PP.plain err)

59+ Left err -> fail (show $ PP.plain $ parseErrorDoc err)

60 Right x -> return x

61 else do

62 putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]

src/Idris/Parser.hs+3−3

@@ -1578,14 +1578,14 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe P.Delta ->

1578parseProg syn fname input mrk

1579 = do i <- getIState

1580 case runparser mainProg i fname input of

1581− Left doc -> do -- FIXME: Get error location from trifecta

1581+ Left err -> do -- FIXME: Get error location from trifecta

1582 -- this can't be the solution!

1583 -- Issue #1575 on the issue tracker.

1584 -- https://github.com/idris-lang/Idris-dev/issues/1575

1585− let (fc, msg) = findFC doc

1585+ let (fc, msg) = findFC $ parseErrorDoc err

1586 i <- getIState

1587 case idris_outputmode i of

1588− RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1588+ RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

1589 IdeMode n h -> iWarn fc (Util.Pretty.text msg)

1590 putIState (i { errSpan = Just fc })

1591 return []

src/Idris/Parser/Expr.hs+1−1

@@ -59,7 +59,7 @@ fullExpr syn = do x <- expr syn

59 return $ debindApp syn (desugar syn i x)

60

61tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

62−tryFullExpr syn st = left (Msg . show) . runparser (fullExpr syn) st ""

62+tryFullExpr syn st = left (Msg . show . parseErrorDoc) . runparser (fullExpr syn) st ""

63

64{- | Parses an expression

65@

src/Idris/Parser/Helpers.hs+2−2

@@ -82,14 +82,14 @@ class HasLastTokenSpan m where

82instance HasLastTokenSpan IdrisParser where

83 getLastTokenSpan = lastTokenSpan <$> get

84

85−type ParseError = PP.Doc

85+newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }

86

87-- | Helper to run Idris inner parser based stateT parsers

88runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res

89runparser p i inputname s =

90 case P.parseString (runInnerParser (evalStateT p i))

91 (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of

92− P.Failure (P.ErrInfo doc _) -> Left doc

92+ P.Failure (P.ErrInfo doc _) -> Left (ParseError doc)

93 P.Success value -> Right value

94

95highlightP :: FC -> OutputAnnotation -> IdrisParser ()

src/Idris/Prover.hs+3−3

@@ -34,6 +34,7 @@ import qualified Idris.IdeMode as IdeMode

34import Idris.Options

35import Idris.Output

36import Idris.Parser hiding (params)

37+import Idris.Parser.Helpers (parseErrorDoc)

37import Idris.TypeSearch (searchByType)

38import Idris.TypeSearch (searchByType)

38

39

39import Util.Pretty

40import Util.Pretty

@@ -43,7 +44,6 @@ import Control.Monad.State.Strict

43import System.Console.Haskeline

44import System.Console.Haskeline

44import System.Console.Haskeline.History

45import System.Console.Haskeline.History

45import System.IO (Handle, hPutStrLn, stdin, stdout)

46import System.IO (Handle, hPutStrLn, stdin, stdout)

46−import qualified Text.Trifecta.Result as P

47

48-- | Launch the proof shell

49prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

@@ -319,7 +319,7 @@ elabloop info fn d prompt prf e prev h env

319 idrisCatch

320 (case cmd of

321 Left err ->

322− return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

322+ return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)

323 Right (Left cmd') ->

324 case cmd' of

325 EQED -> do hs <- lifte e get_holes

@@ -434,7 +434,7 @@ ploop fn d prompt prf e h

434 _ -> return ()

435 (d, st, done, prf', res) <- idrisCatch

436 (case cmd of

437− Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

437+ Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

438 Right Undo -> do (_, st) <- elabStep e loadState

439 return (True, st, False, init prf, Right $ iPrintResult "")

440 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

src/Idris/REPL.hs+3−2

@@ -72,6 +72,7 @@ import Idris.ModeCommon

72import Idris.Options

73import Idris.Output

74import Idris.Parser hiding (indent)

75+import Idris.Parser.Helpers (parseErrorDoc)

75import Idris.Prover

76import Idris.Prover

76import Idris.REPL.Browse (namesInNS, namespacesInNS)

77import Idris.REPL.Browse (namesInNS, namespacesInNS)

77import Idris.REPL.Commands

78import Idris.REPL.Commands

@@ -294,7 +295,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

294 do c <- colourise

295 do c <- colourise

295 i <- getIState

296 i <- getIState

296 case parseCmd i "(input)" cmd of

297 case parseCmd i "(input)" cmd of

297− Left err -> iPrintError $ show (fixColour False err)

298+ Left err -> iPrintError . show . fixColour False . parseErrorDoc $ err

298 Right (Right (Prove mode n')) ->

299 Right (Right (Prove mode n')) ->

299 idrisCatch

300 idrisCatch

300 (do process fn (Prove mode n')

301 (do process fn (Prove mode n')

@@ -726,7 +727,7 @@ processInput cmd orig inputs efile

726 let fn = fromMaybe "" (listToMaybe inputs)

727 let fn = fromMaybe "" (listToMaybe inputs)

727 c <- colourise

728 c <- colourise

728 case parseCmd i "(input)" cmd of

729 case parseCmd i "(input)" cmd of

729− Left err -> Just inputs <$ iputStrLn (show (fixColour c err))

730+ Left err -> Just inputs <$ iputStrLn (show . fixColour c . parseErrorDoc $ err)

730 Right (Right Reload) ->

731 Right (Right Reload) ->

731 reload orig inputs

732 reload orig inputs

732 Right (Right Watch) ->

733 Right (Right Watch) ->

src/Idris/REPL/Parser.hs−1

@@ -33,7 +33,6 @@ import System.Console.ANSI (Color(..))

33import System.FilePath ((</>))

34import Text.Parser.Char (anyChar, oneOf)

35import Text.Parser.Combinators

36−import qualified Text.Trifecta as P

37

36

38parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

37parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

39parseCmd i inputname = IP.runparser pCmd i inputname . trim

38parseCmd i inputname = IP.runparser pCmd i inputname . trim