diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 20:30:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 20:39:09 +0100 |
| commit | 1d39965a694698c3df238fc424203c6b77b067e7 (patch) | |
| tree | fda16c48cca35c65aa5f852f7c9d69bbfeedc965 | |
| parent | 7d3ab7e00453e259939535618e4e10c624a37ec9 (diff) | |
Selecting whole words on double-click in CoqIDE.
Fixes bug #4026.
| -rw-r--r-- | ide/gtk_parsing.ml | 13 | ||||
| -rw-r--r-- | ide/wg_MessageView.ml | 1 | ||||
| -rw-r--r-- | ide/wg_ProofView.ml | 1 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 1 |
4 files changed, 16 insertions, 0 deletions
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index abbd7e6d5..79ccf61a4 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) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 09f1d4453..b32674084 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -48,6 +48,7 @@ let message_view () : message_view = ~source_buffer:buffer ~packing:scroll#add ~editable:false ~cursor_visible:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index a33f2c591..b12d29d6c 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -181,6 +181,7 @@ let proof_view () = let view = GSourceView2.source_view ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in object diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 5d21efd95..8298d9954 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -418,6 +418,7 @@ object (self) self#buffer#end_user_action () initializer + let () = Gtk_parsing.fix_double_click self in let supersed cb _ = let _ = cb () in GtkSignal.stop_emit() |