comparison src/elaborate.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 7ec8dab190a7
children 1a35e75b6967
comparison
equal deleted inserted replaced
1736:7ec8dab190a7 1737:78d7cc9c9b18
4459 4459
4460 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env 4460 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
4461 4461
4462 fun elabFile basis basis_tm topStr topSgn top_tm env file = 4462 fun elabFile basis basis_tm topStr topSgn top_tm env file =
4463 let 4463 let
4464 val () = ModDb.snapshot ()
4465
4464 val () = mayDelay := true 4466 val () = mayDelay := true
4465 val () = delayedUnifs := [] 4467 val () = delayedUnifs := []
4466 val () = delayedExhaustives := [] 4468 val () = delayedExhaustives := []
4467 4469
4468 val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), SOME basis_tm), ErrorMsg.dummySpan) 4470 val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), SOME basis_tm), ErrorMsg.dummySpan)
4786 in 4788 in
4787 ignore (foldl dumpDecl env' file) 4789 ignore (foldl dumpDecl env' file)
4788 end 4790 end
4789 else 4791 else
4790 (); 4792 ();
4793
4794 if ErrorMsg.anyErrors () then
4795 ModDb.revert ()
4796 else
4797 ();
4791 4798
4792 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 4799 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
4793 :: ds 4800 :: ds
4794 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 4801 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
4795 :: ds' @ file 4802 :: ds' @ file