@@ -114,10 +114,15 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
114 addIBC (IBCCoercion n)
114 addIBC (IBCCoercion n)
115 -- If the function is declared as an error handler and the language
115 -- If the function is declared as an error handler and the language
116 -- extension is enabled, then add it to the list of error handlers.
116 -- extension is enabled, then add it to the list of error handlers.
117− when (ErrorReflection `elem` idris_language_extensions i && ErrorHandler `elem` opts) $
117+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
118+ when (ErrorHandler `elem` opts) $ do
118− -- TODO: Check that the declared type is the correct type for an error handler:
121+ -- TODO: Check that the declared type is the correct type for an error handler:
119− -- handler : List (TTName, TT) -> Err -> ErrorReport
122+ -- handler : List (TTName, TT) -> Err -> ErrorReport
120− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
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."
121 when corec $ do setAccessibility n Frozen
126 when corec $ do setAccessibility n Frozen
122 addIBC (IBCAccess n Frozen)
127 addIBC (IBCAccess n Frozen)
123 return usety
128 return usety