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

4 files changed, 16 insertions, 9 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 *)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 0977a1890..9c5b06a0d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -69,6 +69,12 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
 
 let set_location = ref  (function s -> failwith "not ready")
 
+let display_location ins =
+  let line = ins#line + 1 in
+  let off = ins#line_offset + 1 in
+  let msg = Printf.sprintf "Line: %5d Char: %3d" line off in
+  !set_location msg
+
 (** A utf8 char is either a single byte (ascii char, 0xxxxxxx)
     or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *)
 
@@ -465,4 +471,3 @@ let browse_keyword prerr text =
     let u = Lazy.force url_for_keyword text in
     browse prerr (doc_url() ^ u)
   with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
-
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index f06a48aeb..99ff763e2 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -56,6 +56,7 @@ val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
 val set_location : (string -> unit) ref
+val display_location : GText.iter -> unit
 
 (* In win32, when a command-line is to be executed via cmd.exe
    (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
@@ -95,4 +96,3 @@ val io_read_all : Glib.Io.channel -> string
 
 val run_command :
   (string -> unit) -> (Unix.process_status -> unit) -> string -> unit
-
diff --git a/ide/session.ml b/ide/session.ml
index 0a09cc9f5..8dada8ff2 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -209,10 +209,7 @@ let set_buffer_handlers
   let mark_set_cb it m =
     debug_edit_zone ();
     let ins = get_insert () in
-    let line = ins#line + 1 in
-    let off = ins#line_offset + 1 in
-    let msg = Printf.sprintf "Line: %5d Char: %3d" line off in
-    let () = !Ideutils.set_location msg in
+    let () = Ideutils.display_location ins in
     match GtkText.Mark.get_name m with
     | Some "insert" -> ()
     | Some s -> Minilib.log (s^" moved")