From a7a1ec22bc2aa06cc419f7012863656c3aec5871 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Jun 2015 10:49:02 +0200
Subject: STM: silly mistake in jumping back to an old state (Close #4249)

---
 stm/stm.ml                  |  5 +++--
 test-suite/ide/bug4249.fake | 16 ++++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/ide/bug4249.fake

diff --git a/stm/stm.ml b/stm/stm.ml
index fa3ffc7c6e..a6b21bcd9e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2328,9 +2328,9 @@ let edit_at id =
     VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
       (Option.default brname bn)
       (no_edit brinfo.VCS.kind);
-      VCS.print ();
     VCS.delete_cluster_of id;
     VCS.gc ();
+    VCS.print ();
     Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
@@ -2368,7 +2368,8 @@ let edit_at id =
           end else begin
             anomaly(str"Cannot leave an `Edit branch open")
           end
-      | false, None, _ -> backto id None
+      | false, None, Some(_,bn) -> backto id (Some bn)
+      | false, None, None -> backto id None
     in
     VCS.print ();
     rc
diff --git a/test-suite/ide/bug4249.fake b/test-suite/ide/bug4249.fake
new file mode 100644
index 0000000000..20afe0fb8d
--- /dev/null
+++ b/test-suite/ide/bug4249.fake
@@ -0,0 +1,16 @@
+ADD { Lemma a : True. }
+ADD here { Proof using. }
+ADD { fail. }
+ADD { trivial. } # first error
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD fix { trivial. }
+ADD { Qed. }
+WAIT
+EDIT_AT fix
+ADD { Qed. }
+EDIT_AT fix
+ADD { Qed. }
+JOIN
-- 
cgit v1.2.3