dbbdbb2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #662 from hannesm/error-cleanup

dbbdbb2Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+7−16

compare with master

unifiedsplit

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

325ihputStrLn h s = do i <- getIState

326 case idris_outputmode i of

327 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

339

329

340iputStrLn = ihputStrLn stdout

330iputStrLn = ihputStrLn stdout

341iPrintError = ihPrintError stdout

331iPrintError = ihPrintError stdout

342iPrintResult = ihPrintResult stdout

332iPrintResult = ihPrintResult stdout

333+iWarn = ihWarn stdout

343

334

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

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

345ideslavePutSExp cmd info = do i <- getIState

336ideslavePutSExp cmd info = do i <- getIState

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

359 case idris_outputmode i of

350 case idris_outputmode i of

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

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

361

352

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

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

363−iWarn fc err = do i <- getIState

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

364− case idris_outputmode i of

355+ case idris_outputmode i of

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

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

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

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

367

358

368setLogLevel :: Int -> Idris ()

359setLogLevel :: Int -> Idris ()

369setLogLevel l = do i <- getIState

360setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+1−5

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

1612

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

1614elabDecl what info d

1615− = idrisCatch (elabDecl' what info d)

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

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

1617− ist <- getIState

1618− let h = idris_outh ist

1619− ihputStrLn h $ pshow ist e)

1620

1616

1621elabDecl' _ info (PFix _ _ _)

1617elabDecl' _ info (PFix _ _ _)

1622 = return () -- nothing to elaborate

1618 = return () -- nothing to elaborate

src/Idris/Error.hs+8−3

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

35 | isUserError e = ioeGetErrorString e

36 | otherwise = show e

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

39−--idrisCatch = catch

40−

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

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

42idrisCatch = catchError

39idrisCatch = catchError

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

45ifail :: String -> Idris a

50ifail :: String -> Idris a

46ifail = throwError . Msg

51ifail = throwError . Msg

src/Idris/Parser.hs+41−23

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

15import qualified Text.Parser.Char as Chr

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

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

19+

18import Idris.AbsSyntax

20import Idris.AbsSyntax

19import Idris.DSL

21import Idris.DSL

20import Idris.Imports

22import Idris.Imports

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

911 i <- get

913 i <- get

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

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

913

915

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+

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

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

915-- documentation strings.

924-- documentation strings.

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

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

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

919 = do i <- getIState

928 = do i <- getIState

920 case runparser mainProg i fname input of

929 case runparser mainProg i fname input of

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

930 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

923 i <- getIState

933 i <- getIState

934+ case idris_outputmode i of

924− ihputStrLn (idris_outh i) (show doc)

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

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

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

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

926 return []

938 return []

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

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

928 return $ collect x

940 return $ collect x

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

935 i' <- get

947 i' <- get

936 return (ds, i')

948 return (ds, i')

937

949

938−{- | Load idris module -}

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

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

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

940loadModule outh f

952loadModule outh f

941− = idrisCatch (do i <- getIState

953+ = idrisCatch (loadModule' outh f)

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

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

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

961 ist <- getIState

955 ist <- getIState

962 msg <- showErr e

956 msg <- showErr e

963 ihputStrLn outh msg

957 ihputStrLn outh msg

964 return "")

958 return "")

965

959

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+

966{- | Load idris code from file -}

984{- | Load idris code from file -}

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

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

968loadFromIFile h i@(IBC fn src)

986loadFromIFile h i@(IBC fn src)

src/Idris/REPL.hs+51−49

@@ -199,55 +199,57 @@ ideslave orig mods

199 Right (sexp, id) -> return (sexp, id)

200 i <- getIState

201 putIState $ i { idris_outputmode = (IdeSlave id) }

202+ idrisCatch -- to report correct id back!

202− let fn = case mods of

203+ (do let fn = case mods of

203− (f:_) -> f

204+ (f:_) -> f

204− _ -> ""

205+ _ -> ""

205− case IdeSlave.sexpToCommand sexp of

206+ case IdeSlave.sexpToCommand sexp of

206− Just (IdeSlave.Interpret cmd) ->

207+ Just (IdeSlave.Interpret cmd) ->

207− do c <- colourise

208+ do c <- colourise

208− case parseCmd i "(input)" cmd of

209+ case parseCmd i "(input)" cmd of

209− Failure err -> iPrintError $ show (fixColour c err)

210+ Failure err -> iPrintError $ show (fixColour c err)

210− Success (Prove n') -> do iPrintResult ""

211+ Success (Prove n') -> do iPrintResult ""

211− idrisCatch

212+ idrisCatch

212− (process stdout fn (Prove n'))

213+ (process stdout fn (Prove n'))

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

214+ (\e -> getIState >>= iPrintError . flip pshow e)

214− isetPrompt (mkPrompt mods)

215+ isetPrompt (mkPrompt mods)

215− Success cmd -> idrisCatch

216+ Success cmd -> idrisCatch

216− (ideslaveProcess fn cmd)

217+ (ideslaveProcess fn cmd)

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

218+ (\e -> getIState >>= iPrintError . flip pshow e)

218− Just (IdeSlave.REPLCompletions str) ->

219+ Just (IdeSlave.REPLCompletions str) ->

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

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

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

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

221− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

222+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id

222− Just (IdeSlave.LoadFile filename) ->

223+ Just (IdeSlave.LoadFile filename) ->

223− do clearErr

224+ do clearErr

224− putIState (orig { idris_options = idris_options i,

225+ putIState (orig { idris_options = idris_options i,

225− idris_outputmode = (IdeSlave id) })

226+ idris_outputmode = (IdeSlave id) })

226− loadModule stdout filename

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

227− iucheck

228+ return ())

229+ (setAndReport)

228− isetPrompt (mkPrompt [filename])

230+ isetPrompt (mkPrompt [filename])

229−

230− -- Report either success or failure

231+ -- Report either success or failure

231− i <- getIState

232+ i <- getIState

232− case (errLine i) of

233+ case (errLine i) of

233− Nothing -> iPrintResult $ "loaded " ++ filename

234+ Nothing -> iPrintResult $ "loaded " ++ filename

234− Just x -> iPrintError $ "didn't load " ++ filename

235+ Just x -> iPrintError $ "didn't load " ++ filename

235− ideslave orig [filename]

236+ ideslave orig [filename]

236− Just (IdeSlave.TypeOf name) ->

237+ Just (IdeSlave.TypeOf name) ->

237− process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

238+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

238− Just (IdeSlave.CaseSplit line name) ->

239+ Just (IdeSlave.CaseSplit line name) ->

239− process stdout fn (CaseSplitAt False line (UN name))

240+ process stdout fn (CaseSplitAt False line (UN name))

240− Just (IdeSlave.AddClause line name) ->

241+ Just (IdeSlave.AddClause line name) ->

241− process stdout fn (AddClauseFrom False line (UN name))

242+ process stdout fn (AddClauseFrom False line (UN name))

242− Just (IdeSlave.AddProofClause line name) ->

243+ Just (IdeSlave.AddProofClause line name) ->

243− process stdout fn (AddProofClauseFrom False line (UN name))

244+ process stdout fn (AddProofClauseFrom False line (UN name))

244− Just (IdeSlave.AddMissing line name) ->

245+ Just (IdeSlave.AddMissing line name) ->

245− process stdout fn (AddMissing False line (UN name))

246+ process stdout fn (AddMissing False line (UN name))

246− Just (IdeSlave.MakeWithBlock line name) ->

247+ Just (IdeSlave.MakeWithBlock line name) ->

247− process stdout fn (MakeWith False line (UN name))

248+ process stdout fn (MakeWith False line (UN name))

248− Just (IdeSlave.ProofSearch line name hints) ->

249+ Just (IdeSlave.ProofSearch line name hints) ->

249− process stdout fn (DoProofSearch False line (UN name) (map UN hints))

250+ process stdout fn (DoProofSearch False line (UN name) (map UN hints))

250− Nothing -> do iPrintError "did not understand")

251+ Nothing -> do iPrintError "did not understand")

252+ (\e -> do iPrintError $ show e))

251 (\e -> do iPrintError $ show e)

253 (\e -> do iPrintError $ show e)

252 ideslave orig mods

254 ideslave orig mods

253

255