Mercurial > urweb
changeset 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 |
| files | src/elaborate.sml src/mod_db.sig src/mod_db.sml tests/baddep.urp tests/baddep1.ur tests/baddep2.ur |
| diffstat | 6 files changed, 21 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Wed May 02 08:34:50 2012 -0400 +++ b/src/elaborate.sml Wed May 02 08:56:19 2012 -0400 @@ -4461,6 +4461,8 @@ 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 @@ end else (); + + if ErrorMsg.anyErrors () then + ModDb.revert () + else + (); (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds
--- a/src/mod_db.sig Wed May 02 08:34:50 2012 -0400 +++ b/src/mod_db.sig Wed May 02 08:56:19 2012 -0400 @@ -35,4 +35,8 @@ * We might invalidate other declarations that depend on this one, if the timestamp has changed. *) val lookup : Source.decl -> Elab.decl option + + (* Allow undoing to snapshots after failed compilations. *) + val snapshot : unit -> unit + val revert : unit -> unit end
--- 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/baddep.urp Wed May 02 08:56:19 2012 -0400 @@ -0,0 +1,2 @@ +baddep1 +baddep2