diff options
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) |