Email Gateway (Aug 22 2022 at 10:59): Email Gateway (Aug 22 2022 at 10:59):From: Rafal Kolanski <xs@xaph.net>
Hi,
I am having difficulty figuring out what the right forum is to cover
this issue, but in 2012 people were complaining that copy-paste from the
goals / query window does not work if you try select and then
middle-paste. I don't think anyone except Isabelle users really uses
JEdit anymore, so I'll try here.
I've encountered people who assume that this is because "it works in
JEdit and Makarius just overwrote the settings because he doesn't care
about X11 throwbacks or something". This is not the case.
JEdit code instructs plugin authors to use JEditEmbeddedTextArea
(superclass: TextArea), which the JEdit plugin does correctly.
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 all went 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 editing 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.
I'd like to contribute this to the JEdit repository, but there are so
many outstanding patches and bug reports on the sourceforge page that I
don't think there's anyone left who actually cares. Any advice?
If you want to patch this yourself, you can find a version of jEdit
sources in the contrib directory:
e.g. ~/.isabelle/contrib/jedit_build-20150228/contrib/jEdit-patched.tar.gz
Unpack that somewhere.
Go in there (jEdit-patched folder from inside the archive) and do:
patch -p0 < jedit_embeddedtextarea_mousehandler_fix.patch
then:
ant build
That takes about 4-5 minutes the first time as it'll fetch all the sources.
Don't forget to copy the resulting build/jedit.jar over the one in
~/.isabelle/contrib/jedit_build-20150228/contrib/jedit-5.2.0-patched
Happy copy-pasting.
Rafal Kolanski
jedit_embeddedtextarea_mousehandler_fix.patch
Email Gateway (Aug 22 2022 at 11:01):From: Makarius <makarius@sketis.net>
The proper name and spelling of jEdit is "jEdit". Its Sourceforge project
is here: http://sourceforge.net/projects/jedit
There are various trackers to submit artifacts, such as "Patches" for
proposed changes to the main jEdit code base:
http://sourceforge.net/p/jedit/patches
For example, this is what happened to my own submissions in the past few
years: http://sourceforge.net/p/jedit/patches/search/?q=makarius -- it was
mostly "closed-accepted". Only my very first patch was "closed-rejected"
for various reasons.
Discussions about jEdit development often happen right in the tracker
threads -- all of that is copied automatically to the jedit-devel mailing
list. It is also possible to open threads just on the mailing list, e.g.
for general discussions.
Makarius
Email Gateway (Aug 22 2022 at 11:01):From: Rafal Kolanski <xs@xaph.net>
On 28/08/15 21:51, Makarius wrote:
On Thu, 27 Aug 2015, Rafal Kolanski wrote:
I am having difficulty figuring out what the right forum is to cover
this issue, but in 2012 people were complaining that copy-paste from
the goals / query window does not work if you try select and then
middle-paste. I don't think anyone except Isabelle users really uses
JEdit anymore, so I'll try here.The proper name and spelling of jEdit is "jEdit". Its Sourceforge
project is here: http://sourceforge.net/projects/jedit
I think it got stuck after typing JEdit* class names for a week.
There are various trackers to submit artifacts, such as "Patches" for
proposed changes to the main jEdit code base:
http://sourceforge.net/p/jedit/patchesFor example, this is what happened to my own submissions in the past few
years: http://sourceforge.net/p/jedit/patches/search/?q=makarius -- it
was mostly "closed-accepted". Only my very first patch was
"closed-rejected" for various reasons.
Submitted there.
I still welcome comments from you on the actual content, as it affects
Isabelle plugin users mainly. No other plugin uses
JEditEmbeddedTextArea, and so it is a second-class citizen. Note how you
have to rebind ctrl+c yourself to do copy from the output/query buffers.
Another feature that people think is easy, but really isn't for this
reason: how nice it would be to hop over to the output/query buffer with
your keyboard, select some text to copy and hop back.
My small workaround I sent to isabelle-dev received a similar reaction
from you to this one: no discussion of patch content / functionality.
There is no patch tracker to submit that to.
Rafal Kolanski.
Email Gateway (Aug 22 2022 at 11:01):From: Makarius <makarius@sketis.net>
On Sat, 29 Aug 2015, Rafal Kolanski wrote:
Submitted there.
I still welcome comments from you on the actual content, as it affects
Isabelle plugin users mainly. No other plugin uses
JEditEmbeddedTextArea, and so it is a second-class citizen.
I will look at it a bit later. The jEdit guys do care about
JEditEmbeddedTextArea as a separate thing -- they've spent quite some
efforts on it in the past.
My small workaround I sent to isabelle-dev received a similar reaction
from you to this one: no discussion of patch content / functionality.
I did not look at it yet -- I am presently lagging behind 4-8 weeks
concerning various mailing list threads. We don't have real-time
reactivity on the mailing lists. Things are handled eventually, and are
normally not forgotten.
There is no patch tracker to submit that to.
Patch trackers usually slow down reactivity by at least a factor of two.
I experience that routinely on various projects, including jEdit.
The fastest raction I've ever seen was on the Cygwin mailing list -- they
are really old-school, and reject fancy trackers outright.
Makarius
Email Gateway (Aug 22 2022 at 11:01):From: Rafal Kolanski <xs@xaph.net>
On 29/08/15 07:37, Makarius wrote:
Submitted there.
I still welcome comments from you on the actual content, as it affects
Isabelle plugin users mainly. No other plugin uses
JEditEmbeddedTextArea, and so it is a second-class citizen.I will look at it a bit later. The jEdit guys do care about
JEditEmbeddedTextArea as a separate thing -- they've spent quite some
efforts on it in the past.
Of course. It does make perfect sense to have a separate embedded text
area, but in our case so is having the option of a middle ground that
allows the obvious (w.r.t. jEdit shortcut setup) keyboard navigation and
copy/paste setup.
For the mouse, I have made a conservative modification that should be
safe and useful for everyone.
For the keyboard, I have investigated some kind of "if no text area in
an edit pane has focus at present, ask the dockable window manager for
if it has a focused text area we could apply the bound command to". So
then next-char, select-paragraph, copy etc. would work in the output
buffer. Sadly, this approach is a total hack and has the feeling of
swimming upstream against better judgment. Hence my desire for feedback
from those more experienced.
My small workaround I sent to isabelle-dev received a similar reaction
from you to this one: no discussion of patch content / functionality.I did not look at it yet -- I am presently lagging behind 4-8 weeks
concerning various mailing list threads. We don't have real-time
reactivity on the mailing lists. Things are handled eventually, and are
normally not forgotten.
No worries. I apologize and understand, I just really wanted to start
some kind of dialogue with you on this topic. We can resume this in a
while, but for the record, the overall larger situation is:
I am instrumenting Chunk.java a bit to allow access to painting the
glyphs that jEdit already has cached for us. Because they are the
ultimate source of information on chunk positioning in a text area and
already include the necessary font substitutions, we can leverage it to
paint those same glyphs overlaid with text colors from Isabelle.
In that case:
The code in paint_chunk_list (Rich_Text_Area) doesn't have to worry
about fonts and font metrics anymore, only specify glyph colors.
Since the fonts are all resolved already, the painted glyphs will
line up perfectly with the jEdit chunk sizes in the background.
The user_font() setup in Token_Markup doesn't need to request extra
chunk splits based on etc/symbols.
fewer chunks means less memory used and faster draw code
(probably not significant)
19*2 fewer potential entries reserved in the chunk ID for extended
styles. As the limit is 127, that may let us have more Isabelle-based
styles in future that are respected by jEdit's chunk creator
(parser?)
fonts will not need to be specified in etc/symbols at all, making my
earlier workaround patch completely unnecessary by (hopefully)
obviating it with correct design
I'm pretty sure I will have this working in a week for my own setup, as
I have a mental layout that makes me compulsively customize colors and
fonts. What I don't know is if anyone else would be interested in this
change, in particular the creator and primary maintainer of the Isabelle
plugin.
There is no patch tracker to submit that to.
Patch trackers usually slow down reactivity by at least a factor of two.
I experience that routinely on various projects, including jEdit.The fastest raction I've ever seen was on the Cygwin mailing list --
they are really old-school, and reject fancy trackers outright.
Please do not think I'm suggesting we have a patch tracker! I am merely
trying to make sure I am approaching the situation correctly. I have
been away from the Isabelle side of things for a while, and want to
start making constructive contributions again.
This is also why you haven't heard anything from me when Isabelle 2015
was in its release candidate status.
Though I still miss my vim input emulation, I am very impressed with
what you have done.
The editor is still scriptable (earlier this week I implemented a "jump
to first Isabelle error in the file" macro, a "set my color scheme"
macro, a "what markup element does Isabelle think this is" macro).
I was also pondering whether it would be possible to write macros in
Scala, because trying to pass a closure to Isabelle code from the
BeanShell is truly a "just don't" moment.
I'm glad to hear from you, and thank you for your time!
Rafal Kolanski
Email Gateway (Aug 22 2022 at 11:01):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
If I am reading this right, then the inability to copy and middle-paste
from the output window did indeed annoy me for a time, but then I found
that I could work around using CTRL-C/CTRL-V to copy and paste from the
output window into the source code window. This has been very handy
recently when the SMT sledgehammer tools in Isabelle2015 claim that a
proof does not succeed, when in fact it does, if you can only copy and
paste the suggestion.
I personally am not planning on rebuilding jEdit to try the patch,
but I hope Isabelle developers will do so, as it would be nice if it
worked with middle-click as well.
- Gene Stark
Email Gateway (Aug 22 2022 at 11:01):From: Rafal Kolanski <xs@xaph.net>
If you want a weaker version of this functionality right now, for
Isabelle-2015, without recompiling jEdit you can apply the attached
patch with "git apply" in your isabelle source folder. It won't work for
multiple-click select (e.g. triple-click), but it's a passable bandaid
for click-and-drag selection.
I created this so my co-workers had something while I hunted for a more
canonical solution.
I Hope this helps you out for the time being.
Rafal Kolanski
mouse-selection-workaround-in-output-query-window.patch
Last updated: Apr 20 2024 at 08:16 UTC