@@ -1038,56 +1038,53 @@ idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
10381038
10391039loadInputs :: Handle -> [FilePath] -> Idris ()
10401040loadInputs h inputs
1041− = do ist <- getIState
1042− -- if we're in --check and not outputting anything, don't bother
1043− -- loading, as it gets really slow if there's lots of modules in
1044− -- a package (instead, reload all at the end to check for
1045− -- consistency only)
1046− opts <- getCmdLine
1047−
1048− let loadCode = case opt getOutput opts of
1049− [] -> not (NoREPL `elem` opts)
1050− _ -> True
1051−
1052− -- For each ifile list, check it and build ibcs in the same clean IState
1053− -- so that they don't interfere with each other when checking
1054−
1055− let ninputs = zip [1..] inputs
1056− ifiles <- mapM (\(num, input) ->
1057− do putIState ist
1058− v <- verbose
1059−-- when v $ iputStrLn $ "(" ++ show num ++ "/" ++
1060−-- show (length inputs) ++
1061−-- ") " ++ input
1062− modTree <- buildTree
1063− (map snd (take (num-1) ninputs))
1064− input
1065− let ifiles = getModuleFiles modTree
1066− iLOG ("MODULE TREE : " ++ show modTree)
1067− iLOG ("RELOAD: " ++ show ifiles)
1068− when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles
1069− -- return the files that need rechecking
1070− return (if (all ibc ifiles) then ifiles else []))
1071− ninputs
1072− inew <- getIState
1073− -- to check everything worked consistently (in particular, will catch
1074− -- if the ibc version is out of date) if we weren't loading per
1075− -- module
1076− case errLine inew of
1077− Nothing ->
1078− do putIState ist
1079− when (not loadCode) $ tryLoad $ nub (concat ifiles)
1080− _ -> return ()
1081− putIState inew
1082−-- inew <- getIState
1083−-- case errLine inew of
1084−-- Nothing ->
1085−-- -- Then, load all the ibcs again, if there were no errors.
1086−-- do putIState ist
1087−-- modTree <- mapM (buildTree (map snd ninputs)) inputs
1088−-- let ifiless = map getModuleFiles modTree
1089−-- mapM_ loadFromIFile (concat ifiless)
1090−-- _ -> return ()
1041+ = idrisCatch
1042+ (do ist <- getIState
1043+ -- if we're in --check and not outputting anything, don't bother
1044+ -- loading, as it gets really slow if there's lots of modules in
1045+ -- a package (instead, reload all at the end to check for
1046+ -- consistency only)
1047+ opts <- getCmdLine
1048+
1049+ let loadCode = case opt getOutput opts of
1050+ [] -> not (NoREPL `elem` opts)
1051+ _ -> True
1052+
1053+ -- For each ifile list, check it and build ibcs in the same clean IState
1054+ -- so that they don't interfere with each other when checking
1055+
1056+ let ninputs = zip [1..] inputs
1057+ ifiles <- mapM (\(num, input) ->
1058+ do putIState ist
1059+ v <- verbose
1060+ -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++
1061+ -- show (length inputs) ++
1062+ -- ") " ++ input
1063+ modTree <- buildTree
1064+ (map snd (take (num-1) ninputs))
1065+ input
1066+ let ifiles = getModuleFiles modTree
1067+ iLOG ("MODULE TREE : " ++ show modTree)
1068+ iLOG ("RELOAD: " ++ show ifiles)
1069+ when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles
1070+ -- return the files that need rechecking
1071+ return (if (all ibc ifiles) then ifiles else []))
1072+ ninputs
1073+ inew <- getIState
1074+ -- to check everything worked consistently (in particular, will catch
1075+ -- if the ibc version is out of date) if we weren't loading per
1076+ -- module
1077+ case errLine inew of
1078+ Nothing ->
1079+ do putIState ist
1080+ when (not loadCode) $ tryLoad $ nub (concat ifiles)
1081+ _ -> return ()
1082+ putIState inew)
1083+ (\e -> case e of
1084+ At f e -> do setErrLine (fc_line f)
1085+ iputStrLn (show e)
1086+ _ -> do setErrLine 3 -- FIXME! Propagate it
1087+ iputStrLn (show e))
10911088 where -- load all files, stop if any fail
10921089 tryLoad :: [IFileType] -> Idris ()
10931090 tryLoad [] = return ()