diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /ide/gtk_parsing.ml | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'ide/gtk_parsing.ml')
-rw-r--r-- | ide/gtk_parsing.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index abbd7e6d..79ccf61a 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -166,3 +166,16 @@ let find_nearest_backward (cursor:GText.iter) targets = | None -> raise Not_found | Some nearest -> nearest +(** On double-click on a view, select the whole word. This is a workaround for + a deficient word handling in TextView. *) +let fix_double_click self = + let callback ev = match GdkEvent.get_type ev with + | `TWO_BUTTON_PRESS -> + let iter = self#buffer#get_iter `INSERT in + let start, stop = get_word_around iter in + let () = self#buffer#move_mark `INSERT ~where:start in + let () = self#buffer#move_mark `SEL_BOUND ~where:stop in + true + | _ -> false + in + ignore (self#event#connect#button_press ~callback) |