comparison src/mod_db.sml @ 1737:78d7cc9c9b18

Don't modify the module cache after elaboration failures
author Adam Chlipala <adam@chlipala.net>
date Wed, 02 May 2012 08:56:19 -0400
parents ab24a7cb2a64
children b6c4b3484752
comparison
equal deleted inserted replaced
1736:7ec8dab190a7 1737:78d7cc9c9b18
139 SOME (#Decl r) 139 SOME (#Decl r)
140 else 140 else
141 NONE) 141 NONE)
142 | _ => NONE 142 | _ => NONE
143 143
144 val byNameBackup = ref (!byName)
145 val byIdBackup = ref (!byId)
146
147 fun snapshot () = (byNameBackup := !byName; byIdBackup := !byId)
148 fun revert () = (byName := !byNameBackup; byId := !byIdBackup)
149
144 end 150 end