Issue: Cannot copy with mouse from JEditEmbeddedText area into '%' register, but can with JEditTextArea. For the Isabelle plugin, this means copying of goals from the prover output is inconvenient.
JEdit code instructs plugin authors to use JEditEmbeddedTextArea
(superclass: TextArea). For the main text area, JEdit uses
JEditTextArea (superclass: TextArea).
JEditEmbeddedTextArea uses TextAreaMouseHandler for its mouse setup.
JEditTextArea uses MouseHandler (superclass: TextAreaMouseHandler)for
its mouse setup.
Now here's where it goes wrong: someone in the distant past
(pre-2012 where the svn history ends) added the mouse copy-paste
functionality, but only added it in MouseHandler. In fact, as it stands
TextAreaMouseHandler's mouseClicked and mouseReleased are just outdated
versions of those in MouseHandler. They are nearly identical, except for
the copy-paste functionality and some better error checking.
The attached patch updates the TextAreaMouseHandler mouseClicked and
mouseReleased actions to contain all the updated functionality of
MouseHandler, making embedded text areas behave like the main text area
for all mouse selection purposes.
I did leave one difference in: embedded text areas don't send out
anything on the EditBus by default. That should be up to the plugin
authors to do.
General observation: JEditEmbeddedTextArea appears to be a second-class citizen. If you use it in your plugin, even if you enable the caret and set the buffer to writeable, pressing the keybinding for "next-char" will send that message to the last focused text area that has an edit pane (as per the beanshell code that gets executed). Consider if the register viewer used JEditEmbeddedTextArea for its register values editor: you couldn't scroll with your cursor keys, copy/paste/etc. That leaves people using JEditEmbeddedTextArea for their plugins having to guess at and implement their own key bindings, e.g. ctrl+c to copy, even if someone rebound that for the rest of JEdit.
Log in to post a comment.