mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
Remove reloaded modules from the cache
Loading modules explicitly that were already loaded would cause the previous, cached module to be kept, and the new checked one to be thrown away.
This commit is contained in:
parent
ca06580fc6
commit
e338574ea1
@ -53,6 +53,9 @@ findModule n env = runModuleM env (Base.findModule n)
|
||||
-- | Load the module contained in the given file.
|
||||
loadModuleByPath :: FilePath -> ModuleCmd T.Module
|
||||
loadModuleByPath path env = runModuleM (resetModuleEnv env) $ do
|
||||
-- unload the module if it already exists
|
||||
unloadModule path
|
||||
|
||||
m <- Base.loadModuleByPath path
|
||||
setFocusedModule (T.mName m)
|
||||
return m
|
||||
@ -60,6 +63,9 @@ loadModuleByPath path env = runModuleM (resetModuleEnv env) $ do
|
||||
-- | Load the given parsed module.
|
||||
loadModule :: FilePath -> P.Module -> ModuleCmd T.Module
|
||||
loadModule path m env = runModuleM env $ do
|
||||
-- unload the module if it already exists
|
||||
unloadModule path
|
||||
|
||||
let n = P.thing (P.mName m)
|
||||
m' <- loadingModule n (Base.loadModule path m)
|
||||
setFocusedModule (T.mName m')
|
||||
|
@ -163,6 +163,16 @@ addLoadedModule path tm lm
|
||||
, lmModule = tm
|
||||
}
|
||||
|
||||
removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules
|
||||
removeLoadedModule path (LoadedModules ms) = LoadedModules (remove ms)
|
||||
where
|
||||
|
||||
remove (lm:rest)
|
||||
| lmFilePath lm == path = rest
|
||||
| otherwise = lm : remove rest
|
||||
|
||||
remove [] = []
|
||||
|
||||
-- Dynamic Environments --------------------------------------------------------
|
||||
|
||||
-- | Extra information we need to carry around to dynamically extend
|
||||
|
@ -321,6 +321,12 @@ setNameSeeds seeds = ModuleT $ do
|
||||
env <- get
|
||||
set $! env { meNameSeeds = seeds }
|
||||
|
||||
-- | Remove a module from the set of loaded module, by its path.
|
||||
unloadModule :: FilePath -> ModuleM ()
|
||||
unloadModule path = ModuleT $ do
|
||||
env <- get
|
||||
set $! env { meLoadedModules = removeLoadedModule path (meLoadedModules env) }
|
||||
|
||||
loadedModule :: FilePath -> T.Module -> ModuleM ()
|
||||
loadedModule path m = ModuleT $ do
|
||||
env <- get
|
||||
|
Loading…
Reference in New Issue
Block a user