on master help sign in
Proper checking for language extension
commit9c54fc1928443250da5dff753275174b9f667788 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 14 Nov 2013, 17:18 (13 years ago) parent357cd83
1 file changed+9−4
src/Idris/ElabDecls.hs+9−4
src/Idris/ElabDecls.hs+9−4
@@ -98,10 +98,15 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
9898 addIBC (IBCCoercion n)
9999 -- If the function is declared as an error handler and the language
100100 -- extension is enabled, then add it to the list of error handlers.
101− when (ErrorReflection `elem` idris_language_extensions i && ErrorHandler `elem` opts) $
102− -- TODO: Check that the declared type is the correct type for an error handler:
103− -- handler : List (TTName, TT) -> Err -> ErrorReport
104− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
101+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
102+ when (ErrorHandler `elem` opts) $ do
103+ if errorReflection
104+ then do
105+ -- TODO: Check that the declared type is the correct type for an error handler:
106+ -- handler : List (TTName, TT) -> Err -> ErrorReport
107+ i <- getIState
108+ putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
109+ else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
105110 when corec $ do setAccessibility n Frozen
106111 addIBC (IBCAccess n Frozen)
107112 where