diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:41:25 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:41:25 +0100 |
| commit | e0805eac59ee4c6c2eafae1d6b7f91530104f18f (patch) | |
| tree | a36443b6a81e50986b9239f676aee2d5df5f1237 /ide/session.ml | |
| parent | c01b003ca1bc3bf04b538f03dadc59732d89aedc (diff) | |
| parent | 2528533d7877ecf99d880650e1c81c78190ca25d (diff) | |
Merge PR #6625: Update location on tab switch, issue 6624
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 5 |
1 files changed, 1 insertions, 4 deletions
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") |