95960ce · Idris-dev · git.iko.soy

src/Idris/Core/TT.hs+1−1

compare with master

unifiedsplit

@@ -117,7 +117,7 @@ data Err = Msg String

117 | Elaborating String Name Err

118 | ProviderError String

119 | LoadingFailed String Err

120− | ReflectionError [ErrorReportPart]

120+ | ReflectionError [[ErrorReportPart]] Err

121 deriving Eq

122{-!

123deriving instance NFData Err

src/Idris/Delaborate.hs+3−2

@@ -192,8 +192,9 @@ pshow i (Elaborating s n e) = "When elaborating " ++ s ++

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

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

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

195−pshow i (ReflectionError parts) = let parts' = map showPart parts in

195+pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

196− concat (intersperse " " parts')

196+ concat (intersperse "\n" parts') ++

197+ "\nOriginal error:\n" ++ indented (pshow i orig)

197 where showPart :: ErrorReportPart -> String

198 where showPart :: ErrorReportPart -> String

198 showPart (TextPart str) = str

199 showPart (TextPart str) = str

199 showPart (NamePart n) = let colour = idris_colourRepl i in

200 showPart (NamePart n) = let colour = idris_colourRepl i in

src/Idris/ElabDecls.hs+1−1

@@ -122,7 +122,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

122 -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt

123 if tyIsHandler nty'

124 then do i <- getIState

125− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }

125+ putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }

126 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

127 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

128 when corec $ do setAccessibility n Frozen

src/Idris/ElabTerm.hs+7−3

@@ -1375,11 +1375,15 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1375

1376 -- Normalize error handler terms to produce the new messages

1377 ctxt <- getContext

1378− let results = map (normalise ctxt []) (map fst handlers)

1378+ let results = map (normalise ctxt []) (map fst handlers) :: [Term]

1379

1380+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

1381+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results) :: [[Term]]

1382+ errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1380

1383

1381− errorparts <- mapM reifyReportPart (concat (mapMaybe unList (mapMaybe fromTTMaybe results)))

1384+ return $ case errorparts of

1385+ [] -> e

1382− return $ ReflectionError errorparts

1386+ parts -> ReflectionError errorparts e

1383

1387

1384 fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1388 fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1385 fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm

1389 fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm