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/ideutils.ml | |
parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) |
update location on tab switch, issue 6624
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r-- | ide/ideutils.ml | 7 |
1 files changed, 6 insertions, 1 deletions
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") - |