11b0ffa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Introduce "emit"

11b0ffaJason Felice9 years ago

src/Idris/Main.hs+3−4

compare with master

unifiedsplit

@@ -31,7 +31,6 @@ import Idris.REPL.Parser

31import IRTS.CodegenCommon

33import Util.System

34−import qualified Util.Pretty

36import Control.Category

35import Control.Category

37import Control.DeepSeq

36import Control.DeepSeq

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

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

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

197 c <- colourise

196 c <- colourise

198 case parseExpr ist str of

197 case parseExpr ist str of

199− Left err -> do iWarn (errorExtent err) (Util.Pretty.text $ errorMessage err)

198+ Left err -> do emit err

200 runIO $ exitWith (ExitFailure 1)

199 runIO $ exitWith (ExitFailure 1)

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

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

202 exprs

201 exprs

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

273execScript expr = do i <- getIState

272execScript expr = do i <- getIState

274 c <- colourise

273 c <- colourise

275 case parseExpr i expr of

274 case parseExpr i expr of

276− Left err -> do iWarn (errorExtent err) (Util.Pretty.text $ errorMessage err)

275+ Left err -> do emit err

277 runIO $ exitWith (ExitFailure 1)

276 runIO $ exitWith (ExitFailure 1)

278 Right term -> do ctxt <- getContext

277 Right term -> do ctxt <- getContext

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

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

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

300 runInit h

299 runInit h

301 processLine i cmd input clr =

300 processLine i cmd input clr =

302 case parseCmd i input cmd of

301 case parseCmd i input cmd of

303− Left err -> iWarn (errorExtent err) (Util.Pretty.text $ errorMessage err)

302+ Left err -> emit err

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

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

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

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

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

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

src/Idris/Output.hs+8−2

@@ -9,12 +9,12 @@ Maintainer : The Idris Community.

9{-# LANGUAGE FlexibleInstances #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

12−module Idris.Output (clearHighlights, idemodePutSExp, iPrintError, iPrintFunTypes,

12+module Idris.Output (clearHighlights, emit, idemodePutSExp, iPrintError, iPrintFunTypes,

13 iPrintResult, iPrintTermWithType, iputGoal, iputStr, iputStrLn,

14 iRender, iRenderError, iRenderOutput, iRenderResult, iWarn,

15 prettyDocumentedIst, printUndefinedNames, pshow, renderExternal,

16 sendHighlighting, sendParserHighlighting, warnTotality,

17− writeHighlights) where

17+ writeHighlights, OutputDoc(..), Warning(..)) where

19import Idris.AbsSyntax

20import Idris.Colours (hEndColourise, hStartColourise)

@@ -53,6 +53,10 @@ pshow ist err = displayDecorated (consoleDecorate ist) .

54type OutputDoc = Doc OutputAnnotation

56+class Warning a where

57+ warningExtent :: a -> FC

58+ warningMessage :: a -> OutputDoc

59+

56data Ann = AText String | ATagged OutputAnnotation Ann | ASplit Ann Ann

60data Ann = AText String | ATagged OutputAnnotation Ann | ASplit Ann Ann

58iWarn :: FC -> OutputDoc -> Idris ()

62iWarn :: FC -> OutputDoc -> Idris ()

@@ -165,6 +169,8 @@ iWarn fc err =

165 layoutWarning loc (Just src) err = loc <$$> src <$$> err <$$> empty

169 layoutWarning loc (Just src) err = loc <$$> src <$$> err <$$> empty

166 layoutWarning loc Nothing err = loc </> err

170 layoutWarning loc Nothing err = loc </> err

167

171

172+emit :: Warning w => w -> Idris ()

173+emit w = iWarn (warningExtent w) (warningMessage w)

168

174

169iRender :: Doc a -> Idris (SimpleDoc a)

175iRender :: Doc a -> Idris (SimpleDoc a)

170iRender d = do w <- getWidth

176iRender d = do w <- getWidth

src/Idris/Parser.hs+3−5

@@ -13,7 +13,7 @@ Maintainer : The Idris Community.

13{-# OPTIONS_GHC -fwarn-unused-imports #-}

15module Idris.Parser(IdrisParser(..), ImportInfo(..), addReplSyntax, clearParserWarnings,

16− decl, errorExtent, errorMessage, fixColour, loadFromIFile, loadModule, name, opChars, parseElabShellStep, parseConst, parseExpr, parseImports, parseTactic,

16+ decl, fixColour, loadFromIFile, loadModule, name, opChars, parseElabShellStep, parseConst, parseExpr, parseImports, parseTactic,

17 runparser, ParseError, parseErrorDoc) where

19import Idris.AbsSyntax hiding (namespace, params)

@@ -36,7 +36,6 @@ import Idris.Parser.Ops

36import Idris.Termination

37import Idris.Unlit

39−import qualified Util.Pretty

40import Util.System (readSource)

39import Util.System (readSource)

42import Prelude hiding (pi)

41import Prelude hiding (pi)

@@ -1518,10 +1517,9 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]

1518parseProg syn fname input mrk

1517parseProg syn fname input mrk

1519 = do i <- getIState

1518 = do i <- getIState

1520 case runparser mainProg i fname input of

1519 case runparser mainProg i fname input of

1521− Left err -> do let fc = errorExtent err

1520+ Left err -> do emit err

1522− iWarn fc (Util.Pretty.string $ errorMessage err)

1523 i <- getIState

1521 i <- getIState

1524− putIState (i { errSpan = Just fc })

1522+ putIState (i { errSpan = Just (warningExtent err) })

1525 return []

1523 return []

1526 Right (x, i) -> do putIState i

1524 Right (x, i) -> do putIState i

1527 reportParserWarnings

1525 reportParserWarnings

src/Idris/Parser/Stack.hs+7−11

@@ -13,8 +13,6 @@ module Idris.Parser.Stack

13 , runparser

14 -- * Parse errors

15 , ParseError

16− , errorExtent

17− , errorMessage

18 , prettyError

16 , prettyError

19 -- * Mark and restore

17 -- * Mark and restore

20 , Mark

18 , Mark

@@ -35,6 +33,7 @@ module Idris.Parser.Stack

35where

33where

37import Idris.Core.TT (FC(..))

35import Idris.Core.TT (FC(..))

36+import Idris.Output (Warning(..))

39import Control.Arrow (app)

38import Control.Arrow (app)

40import Control.Monad.State.Strict (StateT(..), evalStateT)

39import Control.Monad.State.Strict (StateT(..), evalStateT)

@@ -44,6 +43,7 @@ import qualified Data.List.NonEmpty as NonEmpty

44import Data.Void (Void(..))

43import Data.Void (Void(..))

45import System.FilePath (addTrailingPathSeparator, splitFileName)

44import System.FilePath (addTrailingPathSeparator, splitFileName)

46import qualified Text.Megaparsec as P

45import qualified Text.Megaparsec as P

46+import qualified Util.Pretty as PP

48{- * Parsing -}

@@ -64,15 +64,11 @@ runparser p i inputname s =

65data ParseError = ParseError String (P.ParseError (P.Token String) Void)

67−-- | Retrieve a parse error's FC

67+instance Warning ParseError where

68−errorExtent :: ParseError -> FC

69−errorExtent (ParseError _ err) = sourcePositionFC pos

68+ warningExtent (ParseError _ err) = sourcePositionFC pos

70− where

69+ where

71− (pos NonEmpty.:| _) = P.errorPos err

70+ (pos NonEmpty.:| _) = P.errorPos err

72−

73−-- | A single-line parse error message, including location.

74−errorMessage :: ParseError -> String

75−errorMessage (ParseError _ err) = init (P.parseErrorTextPretty err)

71+ warningMessage (ParseError _ err) = PP.text . init . P.parseErrorTextPretty $ err

77-- | A fully formatted parse error, with caret and bar, etc.

73-- | A fully formatted parse error, with caret and bar, etc.

78prettyError :: ParseError -> String

74prettyError :: ParseError -> String