@@ -443,33 +443,22 @@ pInstances :: [(Bool, Name, Name)] -> Idris ()
443443pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs
444444
445445pDSLs :: [(Name, DSL)] -> Idris ()
446−pDSLs cs = mapM_ (\ (n, c) ->
447− do i <- getIState
448− putIState (i { idris_dsls
449− = addDef n c (idris_dsls i) }))
450− cs
446+pDSLs cs = mapM_ (\ (n, c) -> updateIState (\i ->
447+ i { idris_dsls = addDef n c (idris_dsls i) })) cs
451448
452449pDatatypes :: [(Name, TypeInfo)] -> Idris ()
453−pDatatypes cs = mapM_ (\ (n, c) ->
454− do i <- getIState
455− putIState (i { idris_datatypes
456− = addDef n c (idris_datatypes i) }))
457− cs
450+pDatatypes cs = mapM_ (\ (n, c) -> updateIState (\i ->
451+ i { idris_datatypes = addDef n c (idris_datatypes i) })) cs
458452
459453pOptimise :: [(Name, OptInfo)] -> Idris ()
460−pOptimise cs = mapM_ (\ (n, c) ->
461− do i <- getIState
462− putIState (i { idris_optimisation
463− = addDef n c (idris_optimisation i) }))
464− cs
454+pOptimise cs = mapM_ (\ (n, c) -> updateIState (\i ->
455+ i { idris_optimisation = addDef n c (idris_optimisation i) })) cs
465456
466457pSyntax :: [Syntax] -> Idris ()
467−pSyntax s = do i <- getIState
468− putIState (i { syntax_rules = updateSyntaxRules s (syntax_rules i) })
458+pSyntax s = updateIState (\i -> i { syntax_rules = updateSyntaxRules s (syntax_rules i) })
469459
470460pKeywords :: [String] -> Idris ()
471−pKeywords k = do i <- getIState
472− putIState (i { syntax_keywords = k ++ syntax_keywords i })
461+pKeywords k = updateIState (\i -> i { syntax_keywords = k ++ syntax_keywords i })
473462
474463pObjs :: [(Codegen, FilePath)] -> Idris ()
475464pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs
@@ -493,11 +482,8 @@ pHdrs :: [(Codegen, String)] -> Idris ()
493482pHdrs hs = mapM_ (uncurry addHdr) hs
494483
495484pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
496−pPatdefs ds
497− = mapM_ (\ (n, d) ->
498− do i <- getIState
499− putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))
500− ds
485+pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->
486+ i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
501487
502488pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
503489pDefs reexp syms ds
@@ -507,9 +493,8 @@ pDefs reexp syms ds
507493 TyDecl _ _ -> return ()
508494 _ -> do iLOG $ "SOLVING " ++ show n
509495 solveDeferred n
510− i <- getIState
496+ updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
511497-- logLvl 1 $ "Added " ++ show (n, d')
512− putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
513498 if (not reexp) then do iLOG $ "Not exporting " ++ show n
514499 setAccessibility n Hidden
515500 else iLOG $ "Exporting " ++ show n) ds
@@ -569,9 +554,8 @@ pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris
569554pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds
570555
571556pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()
572−pMDocs ds = mapM_ addMDocStr ds
573− where addMDocStr (n, d) = do ist <- getIState
574− putIState ist { idris_moduledocs = addDef n d (idris_moduledocs ist) }
557+pMDocs ds = mapM_ (\ (n, d) -> updateIState (\i ->
558+ i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds
575559
576560pAccess :: Bool -- ^ Reexporting?
577561 -> [(Name, Accessibility)] -> Idris ()
@@ -579,8 +563,7 @@ pAccess reexp ds
579563 = mapM_ (\ (n, a_in) ->
580564 do let a = if reexp then a_in else Hidden
581565 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
582− updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) }))
583− ds
566+ updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds
584567
585568pFlags :: [(Name, [FnOpt])] -> Idris ()
586569pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds
@@ -592,8 +575,7 @@ pTotal :: [(Name, Totality)] -> Idris ()
592575pTotal ds = mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds
593576
594577pTotCheckErr :: [(FC, String)] -> Idris ()
595−pTotCheckErr es = do ist <- getIState
596− putIState ist { idris_totcheckfail = idris_totcheckfail ist ++ es }
578+pTotCheckErr es = updateIState (\i -> i { idris_totcheckfail = idris_totcheckfail i ++ es })
597579
598580pCG :: [(Name, CGInfo)] -> Idris ()
599581pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds
@@ -614,24 +596,19 @@ pNameHints :: [(Name, Name)] -> Idris ()
614596pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns
615597
616598pMetaInformation :: [(Name, MetaInformation)] -> Idris ()
617−pMetaInformation ds = mapM_ (\ (n, m) ->
618− do i <- getIState
619− putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))
620− ds
599+pMetaInformation ds = mapM_ (\ (n, m) -> updateIState (\i ->
600+ i { tt_ctxt = setMetaInformation n m (tt_ctxt i) })) ds
621601
622602pErrorHandlers :: [Name] -> Idris ()
623−pErrorHandlers ns = do i <- getIState
624− putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ ns }
603+pErrorHandlers ns = updateIState (\i ->
604+ i { idris_errorhandlers = idris_errorhandlers i ++ ns })
625605
626606pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()
627−pFunctionErrorHandlers [] = return ()
628−pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]
629− pFunctionErrorHandlers ns
607+pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->
608+ addFunctionErrorHandlers fn arg [handler]) ns
630609
631610pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()
632−pMetavars ns = do i <- getIState
633− putIState $ i { idris_metavars = L.reverse ns
634− ++ idris_metavars i }
611+pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })
635612
636613----- For Cheapskate and docstrings
637614