From 745669e29695b68b0c6aa9dbe27a835e43c87308 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 Mar 2019 13:54:13 +0100
Subject: [stm] unfocus when edition exits the proof (fix #9431)

---
 stm/stm.ml                  |  5 ++---
 test-suite/ide/reopen1.fake | 22 ++++++++++++++++++++++
 2 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/ide/reopen1.fake

diff --git a/stm/stm.ml b/stm/stm.ml
index 8af1a2ebd2..ab388977a5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -3205,10 +3205,9 @@ let edit_at ~doc id =
   let vcs = VCS.backup () in
   let on_cur_branch id =
     let rec aux cur =
-      if id = cur then true
-      else match VCS.visit cur with
+      match VCS.visit cur with
       | { step = `Fork _ } -> false
-      | { next } -> aux next in
+      | { next } -> if id = cur then true else aux next in
     aux (VCS.get_branch_pos (VCS.current_branch ())) in
   let rec is_pure_aux id =
     let view = VCS.visit id in
diff --git a/test-suite/ide/reopen1.fake b/test-suite/ide/reopen1.fake
new file mode 100644
index 0000000000..2c4f13de86
--- /dev/null
+++ b/test-suite/ide/reopen1.fake
@@ -0,0 +1,22 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping outside the focused zone should signal an unfocus.
+ 
+# first proof
+ADD here { Goal True. }
+ADD here1 { Proof. }
+ADD { Qed. }
+WAIT
+EDIT_AT here1
+EDIT_AT here
+# fwd again
+ADD here2 { Proof. }
+ADD here3 { Qed. }
+WAIT
+EDIT_AT here2
+# Fixing the proof
+ADD { Proof. }
+ADD { trivial. }
+ADD { Qed. }
+JOIN
-- 
cgit v1.2.3