b1537b9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Report errors directly, instead of parsing the string given to ihputStrLn

Still use string parsing for parse errors (there must be a better way to get the source location of a parse failure)

commitb1537b938946adbb45a82bf11aa1fd19dbd71e5e authorHannes Mehnert <hannes@mehnert.org> dateFri 22 Nov 2013, 12:02 (13 years ago) parentddac624

5 files changed+60−49

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7−16 src/Idris/ElabDecls.hs+1−5 src/Idris/Error.hs+8−3 src/Idris/Parser.hs+41−23 src/Idris/REPL.hs+3−2

src/Idris/AbsSyntax.hs+7−16

@@ -325,21 +325,12 @@ ihputStrLn :: Handle -> String -> Idris ()

325325ihputStrLn h s = do i <- getIState

326326 case idris_outputmode i of

327327 RawOutput -> runIO $ hPutStrLn h s

328− IdeSlave n ->

329− case span (/=':') s of

330− (fn, ':':rest) -> case span isDigit rest of

331− ([], ':':msg) -> write

332− ([], msg) -> write

333− (row, ':':rest') ->

334− case span isDigit rest' of

335− ([], msg) -> iWarn (FC fn (read row) 0) msg

336− (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg

337− _ -> write

338− where write = runIO . hPutStrLn h $ convSExp "write-string" s n

328+ IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

339329

340330iputStrLn = ihputStrLn stdout

341331iPrintError = ihPrintError stdout

342332iPrintResult = ihPrintResult stdout

333+iWarn = ihWarn stdout

343334

344335ideslavePutSExp :: SExpable a => String -> a -> Idris ()

345336ideslavePutSExp cmd info = do i <- getIState

@@ -359,11 +350,11 @@ isetPrompt p = do i <- getIState

359350 case idris_outputmode i of

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

361352

362−iWarn :: FC -> String -> Idris ()

363−iWarn fc err = do i <- getIState

364− case idris_outputmode i of

365− RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)

366− IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

353+ihWarn :: Handle -> FC -> String -> Idris ()

354+ihWarn h fc err = do i <- getIState

355+ case idris_outputmode i of

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

357+ IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

367358

368359setLogLevel :: Int -> Idris ()

369360setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+1−5

@@ -1612,11 +1612,7 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds

16121612

16131613elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

16141614elabDecl what info d

1615− = idrisCatch (elabDecl' what info d)

1616− (\e -> do setErrLine (getErrLine e)

1617− ist <- getIState

1618− let h = idris_outh ist

1619− ihputStrLn h $ pshow ist e)

1615+ = idrisCatch (elabDecl' what info d) (setAndReport)

16201616

16211617elabDecl' _ info (PFix _ _ _)

16221618 = return () -- nothing to elaborate

src/Idris/Error.hs+8−3

@@ -35,12 +35,17 @@ report e

3535 | isUserError e = ioeGetErrorString e

3636 | otherwise = show e

3737

38−--idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

39−--idrisCatch = catch

40−

4138idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a

4239idrisCatch = catchError

4340

41+setAndReport :: Err -> Idris ()

42+setAndReport e = do ist <- getIState

43+ let h = idris_outh ist

44+ case e of

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

46+ ihWarn h fc $ pshow ist e

47+ _ -> do setErrLine (getErrLine e)

48+ ihputStrLn h $ pshow ist e

4449

4550ifail :: String -> Idris a

4651ifail = throwError . Msg

src/Idris/Parser.hs+41−23

@@ -15,6 +15,8 @@ import qualified Text.Parser.Token as Tok

1515import qualified Text.Parser.Char as Chr

1616import qualified Text.Parser.Token.Highlight as Hi

1717

18+import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

19+

1820import Idris.AbsSyntax

1921import Idris.DSL

2022import Idris.Imports

@@ -911,6 +913,13 @@ parseImports fname input

911913 i <- get

912914 return ((mname, ps, mrk'), i)

913915

916+-- | There should be a better way of doing this...

917+findFC :: Doc -> (FC, String)

918+findFC x = let s = show (plain x) in

919+ case span (/= ':') s of

920+ (failname, ':':rest) -> case span isDigit rest of

921+ (line, ':':rest') -> (FC failname (read line) 0, drop 2 (dropWhile (/= ':') rest'))

922+

914923-- | A program is a list of declarations, possibly with associated

915924-- documentation strings.

916925parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

@@ -919,10 +928,13 @@ parseProg syn fname input mrk

919928 = do i <- getIState

920929 case runparser mainProg i fname input of

921930 Failure doc -> do -- FIXME: Get error location from trifecta

922− --let errl = sourceLine (errorPos err)

931+ -- this can't be the solution!

932+ let (fc, msg) = findFC doc

923933 i <- getIState

924− ihputStrLn (idris_outh i) (show doc)

925− putIState (i { errLine = Just 0 }) -- Just errl })

934+ case idris_outputmode i of

935+ RawOutput -> ihputStrLn (idris_outh i) (show doc)

936+ IdeSlave n -> ihWarn (idris_outh i) fc msg

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

926938 return []

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

928940 return $ collect x

@@ -935,34 +947,40 @@ parseProg syn fname input mrk

935947 i' <- get

936948 return (ds, i')

937949

938−{- | Load idris module -}

950+{- | Load idris module and show error if something wrong happens -}

939951loadModule :: Handle -> FilePath -> Idris String

940952loadModule outh f

941− = idrisCatch (do i <- getIState

942− let file = takeWhile (/= ' ') f

943− ibcsd <- valIBCSubDir i

944− ids <- allImportDirs

945− fp <- liftIO $ findImport ids ibcsd file

946− if file `elem` imported i

947− then iLOG $ "Already read " ++ file

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

949− case fp of

950− IDR fn -> loadSource outh False fn

951− LIDR fn -> loadSource outh True fn

952− IBC fn src ->

953− idrisCatch (loadIBC fn)

954− (\c -> do iLOG $ fn ++ " failed " ++ show c

955− case src of

956− IDR sfn -> loadSource outh False sfn

957− LIDR sfn -> loadSource outh True sfn)

958− let (dir, fh) = splitFileName file

959− return (dropExtension fh))

953+ = idrisCatch (loadModule' outh f)

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

961955 ist <- getIState

962956 msg <- showErr e

963957 ihputStrLn outh msg

964958 return "")

965959

960+{- | Load idris module -}

961+loadModule' :: Handle -> FilePath -> Idris String

962+loadModule' outh f

963+ = do i <- getIState

964+ let file = takeWhile (/= ' ') f

965+ ibcsd <- valIBCSubDir i

966+ ids <- allImportDirs

967+ fp <- liftIO $ findImport ids ibcsd file

968+ if file `elem` imported i

969+ then iLOG $ "Already read " ++ file

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

971+ case fp of

972+ IDR fn -> loadSource outh False fn

973+ LIDR fn -> loadSource outh True fn

974+ IBC fn src ->

975+ idrisCatch (loadIBC fn)

976+ (\c -> do iLOG $ fn ++ " failed " ++ show c

977+ case src of

978+ IDR sfn -> loadSource outh False sfn

979+ LIDR sfn -> loadSource outh True sfn)

980+ let (dir, fh) = splitFileName file

981+ return (dropExtension fh)

982+

983+

966984{- | Load idris code from file -}

967985loadFromIFile :: Handle -> IFileType -> Idris ()

968986loadFromIFile h i@(IBC fn src)

src/Idris/REPL.hs+3−2

@@ -223,8 +223,9 @@ ideslave orig mods

223223 do clearErr

224224 putIState (orig { idris_options = idris_options i,

225225 idris_outputmode = (IdeSlave id) })

226− loadModule stdout filename

227− iucheck

226+ idrisCatch (do mod <- loadModule' stdout filename

227+ return ())

228+ (setAndReport)

228229 isetPrompt (mkPrompt [filename])

229230

230231 -- Report either success or failure