@@ -223,7 +223,7 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch
223223writeIBC :: FilePath -> FilePath -> Idris ()
224224writeIBC src f
225225 = do
226− logIBC 1 $ "Writing IBC for: " ++ show f
226+ logIBC 2 $ "Writing IBC for: " ++ show f
227227 iReport 2 $ "Writing IBC for: " ++ show f
228228 i <- getIState
229229-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of
@@ -233,8 +233,8 @@ writeIBC src f
233233 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
234234 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
235235 writeArchive f ibcf
236− logIBC 1 "Written")
237− (\c -> do logIBC 1 $ "Failed " ++ pshow i c)
236+ logIBC 2 "Written")
237+ (\c -> do logIBC 2 $ "Failed " ++ pshow i c)
238238 return ()
239239
240240-- | Write a package index containing all the imports in the current
@@ -244,14 +244,14 @@ writePkgIndex :: FilePath -> Idris ()
244244writePkgIndex f
245245 = do i <- getIState
246246 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
247− logIBC 1 $ "Writing package index " ++ show f ++ " including\n" ++
247+ logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++
248248 show (map snd imps)
249249 resetNameIdx
250250 let ibcf = initIBC { ibc_imports = imps }
251251 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
252252 writeArchive f ibcf
253− logIBC 1 "Written")
254− (\c -> do logIBC 1 $ "Failed " ++ pshow i c)
253+ logIBC 2 "Written")
254+ (\c -> do logIBC 2 $ "Failed " ++ pshow i c)
255255 return ()
256256
257257mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
@@ -369,7 +369,7 @@ process :: Bool -- ^ Reexporting
369369process reexp phase archive fn = do
370370 ver <- getEntry 0 "ver" archive
371371 when (ver /= ibcVersion) $ do
372− logIBC 1 "ibc out of date"
372+ logIBC 2 "ibc out of date"
373373 let e = if ver < ibcVersion
374374 then "an earlier" else "a later"
375375 ldir <- runIO $ getIdrisLibDir
@@ -524,10 +524,10 @@ processImports reexp phase ar = do
524524 p -> p
525525 case fp of
526526 LIDR fn -> do
527− logIBC 1 $ "Failed at " ++ fn
527+ logIBC 2 $ "Failed at " ++ fn
528528 ifail "Must be an ibc"
529529 IDR fn -> do
530− logIBC 1 $ "Failed at " ++ fn
530+ logIBC 2 $ "Failed at " ++ fn
531531 ifail "Must be an ibc"
532532 IBC fn src -> loadIBC (reexp && re) phase' fn) fs
533533
@@ -650,7 +650,7 @@ processDefs ar = do
650650 case d' of
651651 TyDecl _ _ -> return ()
652652 _ -> do
653− logIBC 1 $ "SOLVING " ++ show n
653+ logIBC 2 $ "SOLVING " ++ show n
654654 solveDeferred emptyFC n
655655 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
656656 where
@@ -749,9 +749,9 @@ processAccess reexp phase ar = do
749749
750750 if (not reexp)
751751 then do
752− logIBC 1 $ "Not exporting " ++ show n
752+ logIBC 2 $ "Not exporting " ++ show n
753753 setAccessibility n Hidden
754− else logIBC 1 $ "Exporting " ++ show n
754+ else logIBC 2 $ "Exporting " ++ show n
755755 -- Everything should be available at the REPL from
756756 -- things imported publicly
757757 when (phase == IBC_REPL True) $ setAccessibility n Public) ds