@@ -113,23 +113,32 @@ hasValidIBCVersion fp = do
113 Right archive -> do ver <- getEntry 0 "ver" archive
113 Right archive -> do ver <- getEntry 0 "ver" archive
114 return (ver == ibcVersion)
114 return (ver == ibcVersion)
116+data ImpAction = FullLoad | Unhide | NoAction deriving (Eq, Show)
116loadIBC :: Bool -- ^ True = reexport, False = make everything private
118loadIBC :: Bool -- ^ True = reexport, False = make everything private
117 -> IBCPhase
119 -> IBCPhase
118 -> FilePath -> Idris ()
120 -> FilePath -> Idris ()
119loadIBC reexport phase fp
121loadIBC reexport phase fp
120 = do imps <- getImported
122 = do imps <- getImported
121− let redo = case lookup fp imps of
123+ let action = case lookup fp imps of
122− Nothing -> True
124+ Nothing -> FullLoad
123− Just p -> not p && reexport
125+ Just p -> if (not p && reexport) then Unhide else NoAction
124− when redo $
126+ when (action /= NoAction) $ do
125− do logIBC 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport
127+ logIBC 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport
126− archiveFile <- runIO $ B.readFile fp
128+ archiveFile <- runIO $ B.readFile fp
127− case toArchiveOrFail archiveFile of
129+ case toArchiveOrFail archiveFile of
128− Left _ -> ifail $ fp ++ " isn't loadable, it may have an old ibc format.\n"
131+ ifail $ fp ++ " isn't loadable, it may have an old ibc format.\n"
129− ++ "Please clean and rebuild it."
132+ ++ "Please clean and rebuild it."
130− Right archive -> do process reexport phase archive fp
136+ process reexport phase archive fp
131− addImported reexport fp
137+ addImported reexport fp
132−-- dumpTT
138+ Unhide -> do
139+ unhide phase archive
140+ addImported reexport fp
134-- | Load an entire package from its index file
143-- | Load an entire package from its index file
135loadPkgIndex :: String -> Idris ()
144loadPkgIndex :: String -> Idris ()
@@ -324,8 +333,13 @@ getEntry alt f a = case findEntryByPath f a of
324 Nothing -> return alt
333 Nothing -> return alt
325 Just e -> return $! (force . decode . fromEntry) e
334 Just e -> return $! (force . decode . fromEntry) e
336+unhide :: IBCPhase -> Archive -> Idris ()
338+ pImports True phase =<< getEntry [] "ibc_imports" ar
339+ pAccess True phase =<< getEntry [] "ibc_access" ar
327process :: Bool -- ^ Reexporting
341process :: Bool -- ^ Reexporting
328− -> IBCPhase
342+ -> IBCPhase
329 -> Archive -> FilePath -> Idris ()
343 -> Archive -> FilePath -> Idris ()
330process reexp phase i fn = do
344process reexp phase i fn = do
331 ver <- getEntry 0 "ver" i
345 ver <- getEntry 0 "ver" i
@@ -616,7 +630,7 @@ pAccess reexp phase ds
616 else logIBC 1 $ "Exporting " ++ show n
630 else logIBC 1 $ "Exporting " ++ show n
617 -- Everything should be available at the REPL from
631 -- Everything should be available at the REPL from
618 -- things imported publicly
632 -- things imported publicly
619− when (phase == IBC_REPL True) $
633+ when (phase == IBC_REPL True) $
620 setAccessibility n Public
634 setAccessibility n Public