f20f461 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1180 from david-christiansen/ideslave-message-fix

Make missing imports errors follow the IDESlave protocol

commitf20f46164dd4a27b46f7b8a74f1cf38437d43e22 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 2 May 2014, 21:39 (12 years ago) parent89c3853 104635b

6 files changed+21−17

compare with master

unifiedsplit

src/Idris/Chaser.hs+1−1 src/Idris/IBC.hs+1−1 src/Idris/Imports.hs+7−6 src/Idris/Output.hs+3−1 src/Idris/Parser.hs+6−5 src/Idris/REPL.hs+3−3

src/Idris/Chaser.hs+1−1

@@ -82,7 +82,7 @@ buildTree built fp = btree [] fp

8282 iLOG $ "CHASING " ++ show file

8383 ibcsd <- valIBCSubDir i

8484 ids <- allImportDirs

85− fp <- runIO $ findImport ids ibcsd file

85+ fp <- findImport ids ibcsd file

8686 iLOG $ "Found " ++ show fp

8787 mt <- runIO $ getIModTime fp

8888 if (file `elem` built)

src/Idris/IBC.hs+1−1

@@ -300,7 +300,7 @@ pImports fs

300300 = do mapM_ (\f -> do i <- getIState

301301 ibcsd <- valIBCSubDir i

302302 ids <- allImportDirs

303− fp <- runIO $ findImport ids ibcsd f

303+ fp <- findImport ids ibcsd f

304304 if (f `elem` imported i)

305305 then iLOG $ "Already read " ++ f

306306 else do putIState (i { imported = f : imported i })

src/Idris/Imports.hs+7−6

@@ -1,6 +1,7 @@

11module Idris.Imports where

33import Idris.AbsSyntax

4+import Idris.Error

56import Idris.Core.TT

67import Paths_idris

@@ -43,15 +44,15 @@ ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp

4344ibcPathNoFallback :: FilePath -> FilePath -> FilePath

4445ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

4546

46−findImport :: [FilePath] -> FilePath -> FilePath -> IO IFileType

47−findImport [] ibcsd fp = fail $ "Can't find import " ++ fp

47+findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType

48+findImport [] ibcsd fp = ierror . Msg $ "Can't find import " ++ fp

4849findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

49− ibcp <- ibcPathWithFallback ibcsd fp_full

50+ ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full

5051 let idrp = srcPath fp_full

5152 let lidrp = lsrcPath fp_full

52− ibc <- doesFileExist ibcp

53− idr <- doesFileExist idrp

54− lidr <- doesFileExist lidrp

53+ ibc <- runIO $ doesFileExist ibcp

54+ idr <- runIO $ doesFileExist idrp

55+ lidr <- runIO $ doesFileExist lidrp

5556-- when idr $ putStrLn $ idrp ++ " ok"

5657-- when lidr $ putStrLn $ lidrp ++ " ok"

5758-- when ibc $ putStrLn $ ibcp ++ " ok"

src/Idris/Output.hs+3−1

@@ -23,7 +23,9 @@ ihWarn h fc err = do i <- getIState

2323 case idris_outputmode i of

2424 RawOutput ->

2525 do err' <- iRender . fmap (fancifyAnnots i) $

26− text (show fc) <> colon <//> err

26+ if fc_fname fc /= ""

27+ then text (show fc) <> colon <//> err

28+ else err

2729 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

2830 IdeSlave n ->

2931 do err' <- iRender . fmap (fancifyAnnots i) $ err

src/Idris/Parser.hs+6−5

@@ -1158,8 +1158,7 @@ loadModule outh f

11581158 = idrisCatch (loadModule' outh f)

11591159 (\e -> do setErrSpan (getErrSpan e)

11601160 ist <- getIState

1161− msg <- showErr e

1162− ihputStrLn outh msg

1161+ ihWarn outh (getErrSpan e) $ pprintErr ist e

11631162 return "")

11641163

11651164{- | Load idris module -}

@@ -1169,7 +1168,7 @@ loadModule' outh f

11691168 let file = takeWhile (/= ' ') f

11701169 ibcsd <- valIBCSubDir i

11711170 ids <- allImportDirs

1172− fp <- liftIO $ findImport ids ibcsd file

1171+ fp <- findImport ids ibcsd file

11731172 if file `elem` imported i

11741173 then iLOG $ "Already read " ++ file

11751174 else do putIState (i { imported = file : imported i })

@@ -1206,7 +1205,9 @@ loadSource' h lidr r

12061205 = idrisCatch (loadSource h lidr r)

12071206 (\e -> do setErrSpan (getErrSpan e)

12081207 ist <- getIState

1209− ihRenderError h (pprintErr ist e))

1208+ case e of

1209+ At f e' -> ihWarn h f (pprintErr ist e')

1210+ _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

12101211

12111212{- | Load Idris source code-}

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

@@ -1219,7 +1220,7 @@ loadSource h lidr f

12191220 (mname, imports, pos) <- parseImports f file

12201221 ids <- allImportDirs

12211222 ibcsd <- valIBCSubDir i

1222− mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f

1223+ mapM_ (\f -> do fp <- findImport ids ibcsd f

12231224 case fp of

12241225 LIDR fn -> ifail $ "No ibc for " ++ f

12251226 IDR fn -> ifail $ "No ibc for " ++ f

src/Idris/REPL.hs+3−3

@@ -1259,11 +1259,11 @@ loadInputs h inputs

12591259 idris_patdefs = patdefs }))

12601260 (\e -> do i <- getIState

12611261 case e of

1262− At f _ -> do setErrSpan f

1263− ihRenderError stdout $ pprintErr i e

1262+ At f e' -> do setErrSpan f

1263+ ihWarn stdout f $ pprintErr i e'

12641264 ProgramLineComment -> return () -- fail elsewhere

12651265 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1266− iputStrLn (pshow i e))

1266+ ihWarn stdout emptyFC $ pprintErr i e)

12671267 where -- load all files, stop if any fail

12681268 tryLoad :: Bool -> [IFileType] -> Idris ()

12691269 tryLoad keepstate [] = return ()