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 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'stm')

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
-- 
cgit v1.2.3