Mercurial > urweb
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 |