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

src/Idris/AbsSyntax.hs+9−3

compare with master

unifiedsplit

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

632 case idris_outputmode i of

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

634

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

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

636ihWarn h fc err = do i <- getIState

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

637 case idris_outputmode i of

638 case idris_outputmode i of

639+ RawOutput ->

640+ runIO $

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

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

642+ IdeSlave n ->

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

644+ runIO . hPutStrLn h $

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

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

640

646

641setLogLevel :: Int -> Idris ()

647setLogLevel :: Int -> Idris ()

642setLogLevel l = do i <- getIState

648setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+2−2

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

38import Data.Char(isLetter, toLower)

39import Data.List.Split (splitOn)

40

41−import Util.Pretty(pretty)

41+import Util.Pretty(pretty, text)

42

43recheckC fc env t

44 = 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

2000

2001 warnMissing decls ns iname meth

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

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

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

2004 | otherwise = return ()

2005

2006 checkInClass ns meth

src/Idris/Error.hs+1−1

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

44 let h = idris_outh ist

45 case e of

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

47− ihWarn h fc $ pshow ist e

47+ ihWarn h fc $ pprintErr ist e

48 _ -> do setErrLine (getErrLine e)

49 ihputStrLn h $ pshow ist e

50

src/Idris/IdeSlave.hs+4

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

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

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

71

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+

72instance SExpable NameOutput where

76instance SExpable NameOutput where

73 toSExp TypeOutput = SymbolAtom "type"

77 toSExp TypeOutput = SymbolAtom "type"

74 toSExp FunOutput = SymbolAtom "function"

78 toSExp FunOutput = SymbolAtom "function"

src/Idris/Parser.hs+3−2

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

38import Paths_idris

39

40import Util.DynamicLinker

41+import qualified Util.Pretty as P

41

42

42import Idris.Core.TT

43import Idris.Core.TT

43import Idris.Core.Evaluate

44import Idris.Core.Evaluate

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

1119 i <- getIState

1120 i <- getIState

1120 case idris_outputmode i of

1121 case idris_outputmode i of

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

1122 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)

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

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

1124 return []

1125 return []

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

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

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

1187 = idrisCatch (loadSource h lidr r)

1188 = idrisCatch (loadSource h lidr r)

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

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

1189 msg <- showErr e

1190 msg <- showErr e

1190− ihputStrLn h msg)

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

1191

1192

1192{- | Load Idris source code-}

1193{- | Load Idris source code-}

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

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

src/Idris/REPL.hs+2−2

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

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

228 idrisCatch

229 (process stdout fn (Prove n'))

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

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

231 isetPrompt (mkPrompt mods)

232 Success cmd -> idrisCatch

233 (ideslaveProcess fn cmd)

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

1126 (\e -> do i <- getIState

1127 case e of

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

1129− iputStrLn (show e)

1129+ ihRenderError stdout $ pprintErr i e

1130 ProgramLineComment -> return () -- fail elsewhere

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

1132 iputStrLn (pshow i e))