c9fb122 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #883 from david-christiansen/semantic-pprint

Highlight errors in ideslave

commitc9fb1229c8e91f1b06eeee795869be69bfbd6c46 authorEdwin Brady <edwin.brady@gmail.com> dateThu 13 Feb 2014, 20:01 (13 years ago) parent3597433 9d559e9

6 files changed+37−12

compare with master

unifiedsplit

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

src/Idris/AbsSyntax.hs+22−3

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

579579type1Doc :: Doc OutputAnnotation

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

581581

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+

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

583596ihPrintError h s = do i <- getIState

584597 case idris_outputmode i of

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

619632 case idris_outputmode i of

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

621634

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

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

623636ihWarn h fc err = do i <- getIState

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

624638 case idris_outputmode i of

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

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

627646

628647setLogLevel :: Int -> Idris ()

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

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

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

11861187loadSource' h lidr r

11871188 = idrisCatch (loadSource h lidr r)

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

1189− msg <- showErr e

1190− ihputStrLn h msg)

1190+ ist <- getIState

1191+ ihRenderError h (pprintErr ist e))

11911192

11921193{- | Load Idris source code-}

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

src/Idris/REPL.hs+4−3

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

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

228228 idrisCatch

229229 (process stdout fn (Prove n'))

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

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

231231 isetPrompt (mkPrompt mods)

232232 Success cmd -> idrisCatch

233233 (ideslaveProcess fn cmd)

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

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

235235 Just (IdeSlave.REPLCompletions str) ->

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

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

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

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

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

11851185 putIState (i { default_total = True })

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

1187+ when (not runrepl) $ setWidth InfinitelyWide

11871188 mapM_ addLangExt (opt getLanguageExt opts)

11881189 setREPL runrepl

11891190 setQuiet (quiet || isJust script)