Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)

Reviewed-by: ejgallego

2 files changed, 24 insertions, 3 deletions

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