diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 19:43:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 19:43:08 +0100 |
| commit | 154bb6a5134c35caea187b83334c098dbadb4e48 (patch) | |
| tree | 74618de2ebe0484ce675f4527ff8414c6f460c3f /ide/coqide.ml | |
| parent | e9b239881bc32dd15ac53b9463708030c95a9e0c (diff) | |
Fixing bug #3261.
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 78fcbaf8c..1d76ceada 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -591,10 +591,12 @@ let get_current_word term = if term.script#buffer#has_selection then let (start, stop) = term.script#buffer#selection_bounds in term.script#buffer#get_text ~slice:true ~start ~stop () - (** Otherwise try to recover the clipboard *) - else match Ideutils.cb#text with - | Some t -> t - | None -> "" + (** Otherwise try to find the word around the cursor *) + else + let it = term.script#buffer#get_iter_at_mark `INSERT in + let start = find_word_start it in + let stop = find_word_end start in + term.script#buffer#get_text ~slice:true ~start ~stop () let print_branch c l = Format.fprintf c " | @[<hov 1>%a@]=> _@\n" |