on master help sign in
Proper checking for language extension
commit0b6cab7715421293456a15ea0498d8dc4ca7cb8c authorDavid Christiansen <david@davidchristiansen.dk> dateThu 14 Nov 2013, 17:18 (13 years ago) parenta32d59c
1 file changed+9−4
src/Idris/ElabDecls.hs+9−4
src/Idris/ElabDecls.hs+9−4
@@ -114,10 +114,15 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
114114 addIBC (IBCCoercion n)
115115 -- If the function is declared as an error handler and the language
116116 -- extension is enabled, then add it to the list of error handlers.
117− when (ErrorReflection `elem` idris_language_extensions i && ErrorHandler `elem` opts) $
118− -- TODO: Check that the declared type is the correct type for an error handler:
119− -- handler : List (TTName, TT) -> Err -> ErrorReport
120− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
117+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
118+ when (ErrorHandler `elem` opts) $ do
119+ if errorReflection
120+ then do
121+ -- TODO: Check that the declared type is the correct type for an error handler:
122+ -- handler : List (TTName, TT) -> Err -> ErrorReport
123+ i <- getIState
124+ putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
125+ else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
121126 when corec $ do setAccessibility n Frozen
122127 addIBC (IBCAccess n Frozen)
123128 return usety