5987a95 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Report errors loading files using semantic highlighting

commit5987a95a39b3870acee2a7789ca9fc9d8e1ee232 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 12 Feb 2014, 23:52 (13 years ago) parent36527f6

6 files changed+21−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+9−3 src/Idris/ElabDecls.hs+2−2 src/Idris/Error.hs+1−1 src/Idris/IdeSlave.hs+4 src/Idris/Parser.hs+3−2 src/Idris/REPL.hs+2−2

src/Idris/AbsSyntax.hs+9−3

@@ -632,11 +632,17 @@ isetPrompt p = do i <- getIState

632632 case idris_outputmode i of

633633 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

634634

635−ihWarn :: Handle -> FC -> String -> Idris ()

635+ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

636636ihWarn h fc err = do i <- getIState

637+ err' <- iRender . fmap (fancifyAnnots i) $ err

637638 case idris_outputmode i of

638− RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)

639− IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n

639+ RawOutput ->

640+ runIO $

641+ hPutStrLn h (show fc ++ ":" ++ displayDecorated (consoleDecorate i) err')

642+ IdeSlave n ->

643+ do let (str, spans) = displaySpans err'

644+ runIO . hPutStrLn h $

645+ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, str, spans) n

640646

641647setLogLevel :: Int -> Idris ()

642648setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+2−2

@@ -38,7 +38,7 @@ import qualified Data.Text as T

3838import Data.Char(isLetter, toLower)

3939import Data.List.Split (splitOn)

4040

41−import Util.Pretty(pretty)

41+import Util.Pretty(pretty, text)

4242

4343recheckC fc env t

4444 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

@@ -2000,7 +2000,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20002000

20012001 warnMissing decls ns iname meth

20022002 | null $ filter (clauseFor meth iname ns) decls

2003− = iWarn fc $ "method " ++ show meth ++ " not defined"

2003+ = iWarn fc . text $ "method " ++ show meth ++ " not defined"

20042004 | otherwise = return ()

20052005

20062006 checkInClass ns meth

src/Idris/Error.hs+1−1

@@ -44,7 +44,7 @@ setAndReport e = do ist <- getIState

4444 let h = idris_outh ist

4545 case e of

4646 At fc@(FC f l c) e -> do setErrLine l

47− ihWarn h fc $ pshow ist e

47+ ihWarn h fc $ pprintErr ist e

4848 _ -> do setErrLine (getErrLine e)

4949 ihputStrLn h $ pshow ist e

5050

src/Idris/IdeSlave.hs+4

@@ -69,6 +69,10 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where

6969instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where

7070 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]

7171

72+instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>

73+ SExpable (a, b, c, d, e) where

74+ toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]

75+

7276instance SExpable NameOutput where

7377 toSExp TypeOutput = SymbolAtom "type"

7478 toSExp FunOutput = SymbolAtom "function"

src/Idris/Parser.hs+3−2

@@ -38,6 +38,7 @@ import Idris.ParseData

3838import Paths_idris

3939

4040import Util.DynamicLinker

41+import qualified Util.Pretty as P

4142

4243import Idris.Core.TT

4344import Idris.Core.Evaluate

@@ -1119,7 +1120,7 @@ parseProg syn fname input mrk

11191120 i <- getIState

11201121 case idris_outputmode i of

11211122 RawOutput -> ihputStrLn (idris_outh i) (show doc)

1122− IdeSlave n -> ihWarn (idris_outh i) fc msg

1123+ IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

11231124 putIState (i { errLine = Just (fc_line fc) }) -- Just errl })

11241125 return []

11251126 Success (x, i) -> do putIState i

@@ -1187,7 +1188,7 @@ loadSource' h lidr r

11871188 = idrisCatch (loadSource h lidr r)

11881189 (\e -> do setErrLine (getErrLine e)

11891190 msg <- showErr e

1190− ihputStrLn h msg)

1191+ ihputStrLn h (msg ++ "fel"))

11911192

11921193{- | Load Idris source code-}

11931194loadSource :: Handle -> Bool -> FilePath -> Idris ()

src/Idris/REPL.hs+2−2

@@ -227,7 +227,7 @@ ideslave orig mods

227227 Success (Prove n') -> do iPrintResult ""

228228 idrisCatch

229229 (process stdout fn (Prove n'))

230− (\e -> getIState >>= ihRenderError . flip pprintErr e)

230+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

231231 isetPrompt (mkPrompt mods)

232232 Success cmd -> idrisCatch

233233 (ideslaveProcess fn cmd)

@@ -1126,7 +1126,7 @@ loadInputs h inputs

11261126 (\e -> do i <- getIState

11271127 case e of

11281128 At f _ -> do setErrLine (fc_line f)

1129− iputStrLn (show e)

1129+ ihRenderError stdout $ pprintErr i e

11301130 ProgramLineComment -> return () -- fail elsewhere

11311131 _ -> do setErrLine 3 -- FIXME! Propagate it

11321132 iputStrLn (pshow i e))