diff options
author | Paul Steckler <steck@stecksoft.com> | 2018-01-19 16:43:14 -0500 |
---|---|---|
committer | Paul Steckler <steck@stecksoft.com> | 2018-01-19 16:43:14 -0500 |
commit | 2528533d7877ecf99d880650e1c81c78190ca25d (patch) | |
tree | 5e718fcebef511915a47bb35e4585624debf52b8 /ide/coqide.ml | |
parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) |
update location on tab switch, issue 6624
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r-- | ide/coqide.ml | 11 |
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 *) |