c9fb122 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+22−3

compare with master

unifiedsplit

@@ -579,6 +579,19 @@ fancifyAnnots _ annot = annot

579type1Doc :: Doc OutputAnnotation

580type1Doc = (annotate AnnConstType $ text "Type 1")

581

582+-- | Show an error with semantic highlighting

583+ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

584+ihRenderError h e = do ist <- getIState

585+ case idris_outputmode ist of

586+ RawOutput -> consoleDisplayAnnotated h e

587+ IdeSlave n -> do

588+ (str, spans) <- fmap displaySpans .

589+ iRender .

590+ fmap (fancifyAnnots ist) $

591+ e

592+ let good = [SymbolAtom "error", toSExp str, toSExp spans]

593+ runIO . hPutStrLn h $ convSExp "return" good n

594+

582ihPrintError :: Handle -> String -> Idris ()

595ihPrintError :: Handle -> String -> Idris ()

583ihPrintError h s = do i <- getIState

596ihPrintError h s = do i <- getIState

584 case idris_outputmode i of

597 case idris_outputmode i of

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

619 case idris_outputmode i of

632 case idris_outputmode i of

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

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

621

634

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

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

623ihWarn h fc err = do i <- getIState

636ihWarn h fc err = do i <- getIState

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

624 case idris_outputmode i of

638 case idris_outputmode i of

639+ RawOutput ->

640+ runIO $

625− 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 $

626− 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

627

646

628setLogLevel :: Int -> Idris ()

647setLogLevel :: Int -> Idris ()

629setLogLevel 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+4−3

@@ -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

@@ -1186,8 +1187,8 @@ loadSource' :: Handle -> Bool -> FilePath -> Idris ()

1186loadSource' h lidr r

1187loadSource' 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+ ist <- getIState

1190− ihputStrLn h msg)

1191+ ihRenderError h (pprintErr ist e))

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+4−3

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

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

228 idrisCatch

229 (process stdout fn (Prove n'))

230− (\e -> getIState >>= iPrintError . flip pshow e)

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

231 isetPrompt (mkPrompt mods)

232 Success cmd -> idrisCatch

233 (ideslaveProcess fn cmd)

234− (\e -> getIState >>= iPrintError . flip pshow e)

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

235 Just (IdeSlave.REPLCompletions str) ->

236 do (unused, compls) <- replCompletion (reverse str, "")

237 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

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

@@ -1184,6 +1184,7 @@ idrisMain opts =

1184 when (DefaultTotal `elem` opts) $ do i <- getIState

1185 putIState (i { default_total = True })

1186 setColourise $ not quiet && last (True : opt getColour opts)

1187+ when (not runrepl) $ setWidth InfinitelyWide

1187 mapM_ addLangExt (opt getLanguageExt opts)

1188 mapM_ addLangExt (opt getLanguageExt opts)

1188 setREPL runrepl

1189 setREPL runrepl

1189 setQuiet (quiet || isJust script)

1190 setQuiet (quiet || isJust script)