Move universe level check to after all modules are loaded
...otherwise it gets repeated needlessly for every module
commit2d8e5733fa8b0545dd8a8b49e959b90697395d28
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 15 Aug 2013, 12:17 (13 years ago)
parent8f8ab98
src/Idris/Parser.hs−2
@@ -129,8 +129,6 @@ loadSource lidr f
129129 iLOG ("Finished " ++ f)
130130 ibcsd <- valIBCSubDir i
131131 let ibc = ibcPathNoFallback ibcsd f
132− iLOG "Universe checking"
133− iucheck
134132 i <- getIState
135133 addHides (hide_list i)
136134 ok <- noErrors
src/Idris/REPL.hs+2
@@ -708,6 +708,8 @@ idrisMain opts =
708708 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
709709 ist <- getIState
710710 mods <- mapM loadModule inputs
711+ iLOG "Universe checking"
712+ iucheck
711713 ok <- noErrors
712714 when ok $ case output of
713715 [] -> return ()