b83793e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #561 from david-christiansen/issue/560

Add an exception handler to main

commitb83793e34c24735fcb2a77f261bbee7a9f4989d2 authorEdwin Brady <edwin.brady@gmail.com> dateThu 24 Oct 2013, 07:37 (13 years ago) parentc261501 9e5c96f

4 files changed+10−2

compare with master

unifiedsplit

src/Core/TT.hs+4 src/Idris/Delaborate.hs+1 src/Idris/Parser.hs+1−1 src/Main.hs+4−1

src/Core/TT.hs+4

@@ -101,6 +101,7 @@ data Err = Msg String

101101 | At FC Err

102102 | Elaborating String Name Err

103103 | ProviderError String

104+ | LoadingFailed String Err

104105 deriving Eq

105106

106107instance Sized Err where

@@ -122,6 +123,7 @@ instance Sized Err where

122123 size (At fc err) = size fc + size err

123124 size (Elaborating _ n err) = size err

124125 size (ProviderError msg) = length msg

126+ size (LoadingFailed fn e) = 1 + length fn + size e

125127 size _ = 1

126128

127129score :: Err -> Int

@@ -139,6 +141,7 @@ instance Show Err where

139141 ++ show e ++ " in " ++ show sc ++ " " ++ show i

140142 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

141143 show (ProviderError msg) = "Type provider error: " ++ msg

144+ show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ show e

142145 show _ = "Error"

143146

144147instance Pretty Err where

@@ -152,6 +155,7 @@ instance Pretty Err where

152155 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

153156 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

154157 pretty (ProviderError msg) = text msg

158+ pretty err@(LoadingFailed _ _) = text (show err)

155159 pretty _ = text "Error"

156160

157161instance Error Err where

src/Idris/Delaborate.hs+1

@@ -163,6 +163,7 @@ pshow i (At f e) = show f ++ ":" ++ pshow i e

163163pshow i (Elaborating s n e) = "When elaborating " ++ s ++

164164 showqual i n ++ ":\n" ++ pshow i e

165165pshow i (ProviderError msg) = "Type provider error: " ++ msg

166+pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e

166167

167168showSc i [] = ""

168169showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/Parser.hs+1−1

@@ -952,7 +952,7 @@ loadFromIFile :: IFileType -> Idris ()

952952loadFromIFile i@(IBC fn src)

953953 = do iLOG $ "Skipping " ++ getSrcFile i

954954 idrisCatch (loadIBC fn)

955− (\c -> do fail $ fn ++ " failed " ++ show c)

955+ (\err -> ierror $ LoadingFailed fn err)

956956 where

957957 getSrcFile (IDR fn) = fn

958958 getSrcFile (LIDR fn) = fn

src/Main.hs+4−1

@@ -40,7 +40,10 @@ import Paths_idris

4040

4141main = do xs <- getArgs

4242 let opts = parseArgs xs

43− runErrorT $ execStateT (runIdris opts) idrisInit

43+ result <- runErrorT $ execStateT (runIdris opts) idrisInit

44+ case result of

45+ Left err -> putStrLn $ "Uncaught error: " ++ show err

46+ Right _ -> return ()

4447

4548runIdris :: [Opt] -> Idris ()

4649runIdris opts = do