Merge PR #6625: Update location on tab switch, issue 6624

1 files changed, 8 insertions, 3 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 842d06859..3cc46b6aa 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1221,9 +1221,14 @@ let build_ui () =
   (* Emacs/PG mode *)
   NanoPG.init w notebook all_menus;
 
-  (* Reset on tab switch *)
-  let _ = notebook#connect#switch_page ~callback:(fun _ ->
-    if reset_on_tab_switch#get then Nav.restart ())
+  (* On tab switch, reset, update location *)
+  let _ = notebook#connect#switch_page ~callback:(fun n ->
+    let _ = if reset_on_tab_switch#get then Nav.restart () in
+    try
+      let session = notebook#get_nth_term n in
+      let ins = session.buffer#get_iter_at_mark `INSERT in
+      Ideutils.display_location ins
+    with _ -> ())
   in
 
   (* Vertical Separator between Scripts and Goals *)