diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-13 11:14:54 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-13 11:15:59 +0100 |
commit | 8f73830d46d985906deadae3059db75772281516 (patch) | |
tree | b993e25a13f7e3d7a0ed3fbb5b4532d6566b04fa /ide | |
parent | 7c9938cfbd0cf9093f90b0ee7b856105528c2a87 (diff) |
Selection of the current word in CoqIDE looks at all buffers.
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coqide.ml | 15 | ||||
-rw-r--r-- | ide/wg_ProofView.ml | 4 | ||||
-rw-r--r-- | ide/wg_ProofView.mli | 1 |
3 files changed, 17 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 1d76ceada..5aac8f2a1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -588,9 +588,18 @@ let get_current_word term = | Some p -> p | None -> (** Then look at the current selected word *) - 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 () + let buf1 = term.script#buffer in + let buf2 = term.proof#buffer in + let buf3 = term.messages#buffer in + if buf1#has_selection then + let (start, stop) = buf1#selection_bounds in + buf1#get_text ~slice:true ~start ~stop () + else if buf2#has_selection then + let (start, stop) = buf2#selection_bounds in + buf2#get_text ~slice:true ~start ~stop () + else if buf3#has_selection then + let (start, stop) = buf3#selection_bounds in + buf3#get_text ~slice:true ~start ~stop () (** Otherwise try to find the word around the cursor *) else let it = term.script#buffer#get_iter_at_mark `INSERT in diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 7e7a311ed..a33f2c591 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -9,6 +9,7 @@ class type proof_view = object inherit GObj.widget + method buffer : GText.buffer method refresh : unit -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit @@ -176,6 +177,7 @@ let proof_view () = ~highlight_matching_brackets:true ~tag_table:Tags.Proof.table () in + let text_buffer = new GText.buffer buffer#as_buffer in let view = GSourceView2.source_view ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD () in @@ -186,6 +188,8 @@ let proof_view () = val mutable goals = None val mutable evars = None + method buffer = text_buffer + method clear () = buffer#set_text "" method set_goals gls = goals <- gls diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index 1fbf9900c..c5e042ea5 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -9,6 +9,7 @@ class type proof_view = object inherit GObj.widget + method buffer : GText.buffer method refresh : unit -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit |