git.iko.soy/Idris-dev
on master help sign in
Move universe level check to after all modules are loaded
2d8e573Edwin Brady
src/Idris/Parser.hs−2
compare with master
unifiedsplit
@@ -129,8 +129,6 @@ loadSource lidr f
129 iLOG ("Finished " ++ f)
129 iLOG ("Finished " ++ f)
130 ibcsd <- valIBCSubDir i
130 ibcsd <- valIBCSubDir i
131 let ibc = ibcPathNoFallback ibcsd f
131 let ibc = ibcPathNoFallback ibcsd f
132− iLOG "Universe checking"
133− iucheck
134 i <- getIState
132 i <- getIState
135 addHides (hide_list i)
133 addHides (hide_list i)
136 ok <- noErrors
134 ok <- noErrors
src/Idris/REPL.hs+2
@@ -708,6 +708,8 @@ idrisMain opts =
708 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
708 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
709 ist <- getIState
709 ist <- getIState
710 mods <- mapM loadModule inputs
710 mods <- mapM loadModule inputs
711+ iLOG "Universe checking"
712+ iucheck
711 ok <- noErrors
713 ok <- noErrors
712 when ok $ case output of
714 when ok $ case output of
713 [] -> return ()
715 [] -> return ()