From 1fd7e4392db0bace167853850188c464b00a8126 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 2 May 2012 08:56:19 -0400
Subject: Don't modify the module cache after elaboration failures

---
 src/elaborate.sml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 26ec21ec..41e9e9ab 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4461,6 +4461,8 @@ fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
 
 fun elabFile basis basis_tm topStr topSgn top_tm env file =
     let
+        val () = ModDb.snapshot ()
+
         val () = mayDelay := true
         val () = delayedUnifs := []
         val () = delayedExhaustives := []
@@ -4788,6 +4790,11 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
             end
         else
             ();
+
+        if ErrorMsg.anyErrors () then
+            ModDb.revert ()
+        else
+            ();
         
         (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
         :: ds
-- 
cgit v1.2.3