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

git.iko.soy/Idris-dev

Introduce "emit"

commit11b0ffac84e7c83202e108b619c01a2e6e343096 authorJason Felice <jason.m.felice@gmail.com> dateMon 11 Dec 2017, 15:58 (9 years ago) parent0a7fe41

4 files changed+21−22

compare with master

unifiedsplit

src/Idris/Main.hs+3−4 src/Idris/Output.hs+8−2 src/Idris/Parser.hs+3−5 src/Idris/Parser/Stack.hs+7−11

src/Idris/Main.hs+3−4

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

3131import IRTS.CodegenCommon

3232

3333import Util.System

34−import qualified Util.Pretty

3534

3635import Control.Category

3736import Control.DeepSeq

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

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

197196 c <- colourise

198197 case parseExpr ist str of

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

198+ Left err -> do emit err

200199 runIO $ exitWith (ExitFailure 1)

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

202201 exprs

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

273272execScript expr = do i <- getIState

274273 c <- colourise

275274 case parseExpr i expr of

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

275+ Left err -> do emit err

277276 runIO $ exitWith (ExitFailure 1)

278277 Right term -> do ctxt <- getContext

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

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

300299 runInit h

301300 processLine i cmd input clr =

302301 case parseCmd i input cmd of

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

302+ Left err -> emit err

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

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

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

src/Idris/Output.hs+8−2

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

99{-# LANGUAGE FlexibleInstances #-}

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

1111

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

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

1313 iPrintResult, iPrintTermWithType, iputGoal, iputStr, iputStrLn,

1414 iRender, iRenderError, iRenderOutput, iRenderResult, iWarn,

1515 prettyDocumentedIst, printUndefinedNames, pshow, renderExternal,

1616 sendHighlighting, sendParserHighlighting, warnTotality,

17− writeHighlights) where

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

1818

1919import Idris.AbsSyntax

2020import Idris.Colours (hEndColourise, hStartColourise)

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

5353

5454type OutputDoc = Doc OutputAnnotation

5555

56+class Warning a where

57+ warningExtent :: a -> FC

58+ warningMessage :: a -> OutputDoc

59+

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

5761

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

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

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

166170 layoutWarning loc Nothing err = loc </> err

167171

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

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

168174

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

170176iRender d = do w <- getWidth

src/Idris/Parser.hs+3−5

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

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

1414

1515module 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,

1717 runparser, ParseError, parseErrorDoc) where

1818

1919import Idris.AbsSyntax hiding (namespace, params)

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

3636import Idris.Termination

3737import Idris.Unlit

3838

39−import qualified Util.Pretty

4039import Util.System (readSource)

4140

4241import Prelude hiding (pi)

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

15181517parseProg syn fname input mrk

15191518 = do i <- getIState

15201519 case runparser mainProg i fname input of

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

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

1520+ Left err -> do emit err

15231521 i <- getIState

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

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

15251523 return []

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

15271525 reportParserWarnings

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

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

1313 , runparser

1414 -- * Parse errors

1515 , ParseError

16− , errorExtent

17− , errorMessage

1816 , prettyError

1917 -- * Mark and restore

2018 , Mark

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

3533where

3634

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

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

3837

3938import Control.Arrow (app)

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

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

4443import Data.Void (Void(..))

4544import System.FilePath (addTrailingPathSeparator, splitFileName)

4645import qualified Text.Megaparsec as P

46+import qualified Util.Pretty as PP

4747

4848{- * Parsing -}

4949

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

6464

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

6666

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

68−errorExtent :: ParseError -> FC

69−errorExtent (ParseError _ err) = sourcePositionFC pos

70− where

71− (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)

67+instance Warning ParseError where

68+ warningExtent (ParseError _ err) = sourcePositionFC pos

69+ where

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

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

7672

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

7874prettyError :: ParseError -> String