diff 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
line wrap: on
line diff
--- a/src/mod_db.sml	Wed May 02 08:34:50 2012 -0400
+++ b/src/mod_db.sml	Wed May 02 08:56:19 2012 -0400
@@ -141,4 +141,10 @@
                  NONE)
       | _ => NONE
 
+val byNameBackup = ref (!byName)
+val byIdBackup = ref (!byId)
+
+fun snapshot () = (byNameBackup := !byName; byIdBackup := !byId)
+fun revert () = (byName := !byNameBackup; byId := !byIdBackup)
+
 end