| 60 |
|
|
| 61 |
(* Evict all elements that belong to a given group but which |
(* Evict all elements that belong to a given group but which |
| 62 |
* are not of the current generation. "cleanGroup" should be |
* are not of the current generation. "cleanGroup" should be |
| 63 |
* called right after finishing to parse the group file. *) |
* called right after finishing to parse the group file. |
| 64 |
val cleanGroup : SrcPath.t -> unit |
* If the boolean flag ("nowStable") is set to true, then all |
| 65 |
|
* members of the group are dismissed regardless of their |
| 66 |
|
* generation. This is used to get rid of the information for |
| 67 |
|
* members of now-stable libraries. *) |
| 68 |
|
val cleanGroup : bool -> SrcPath.t -> unit |
| 69 |
|
|
| 70 |
(* Delete all known info. *) |
(* Delete all known info. *) |
| 71 |
val reset : unit -> unit |
val reset : unit -> unit |
| 154 |
fun forgetParsetree (INFO { persinfo = PERS { parsetree, ... }, ... }) = |
fun forgetParsetree (INFO { persinfo = PERS { parsetree, ... }, ... }) = |
| 155 |
parsetree := NONE |
parsetree := NONE |
| 156 |
|
|
| 157 |
fun cleanGroup g = let |
fun cleanGroup nowStable g = let |
| 158 |
val n = now () |
val n = now () |
| 159 |
fun isCurrent (PERS { generation = ref gen, group = (g', _), ... }) = |
fun isCurrent (PERS { generation = ref gen, group = (g', _), ... }) = |
| 160 |
gen = n orelse SrcPath.compare (g, g') <> EQUAL |
((not nowStable) andalso gen = n) |
| 161 |
|
orelse SrcPath.compare (g, g') <> EQUAL |
| 162 |
in |
in |
| 163 |
knownInfo := SrcPathMap.filter isCurrent (!knownInfo) |
knownInfo := SrcPathMap.filter isCurrent (!knownInfo) |
| 164 |
end |
end |
Parent Directory
| 
Revision Log
| 
Patch
