Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Cannot copy from output panel in Isabelle 2016?


view this post on Zulip Email Gateway (Aug 22 2022 at 12:55):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,

I have just upgraded to Isabelle 2016 from Isabelle 2015 in the last
few days and I have noticed that I cannot copy text from the output
panel/proof state into the jEdit editor pane. I didn't previously
have this problem with Isabelle 2015 and was wondering whether this is
a known problem, and if there is a workaround for it as it is
impacting my ability to work efficiently? I am using Ubuntu 14.04
LTS.

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 12:55):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
This came up in a previous thread several months ago.
At that time, the poster offered a patch to JEdit code, and seemed to
indicate that there was code in the pipeline for JEdit that would fix this.
But it seems that Isabelle2016 is the same as Isabelle2015 in this respect
(AFAIK, Isabelle2015 also has this problem, contrary to what you suggest).

The workaround I use (under Ubuntu 14.04 LTS) is to select highlighted
text using CTRL-C, then paste into the editor window using CTRL-V.

The previous thread can be found at:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-August/msg00160.html

The "References:" header from the previous thread is:

References: <55DE69C5.6020807@xaph.net> <alpine.LNX.2.00.1508281339040.19033@lxbroy10.informatik.tu-muenchen.de> <55E0BEC5.4010609@xaph.net> <55E0E419.5030307@starkeffect.com>

I would have added these to the headers of this message, except that Thunderbird
does not seem to provide me with the ability to do so.

- Gene Stark

On 03/10/2016 05:25 AM, Dominic Mulligan via Cl-isabelle-users wrote:

Hi,

I have just upgraded to Isabelle 2016 from Isabelle 2015 in the last
few days and I have noticed that I cannot copy text from the output
panel/proof state into the jEdit editor pane. I didn't previously
have this problem with Isabelle 2015 and was wondering whether this is
a known problem, and if there is a workaround for it as it is
impacting my ability to work efficiently? I am using Ubuntu 14.04
LTS.

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 12:55):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Gene,

Thanks for your quick reply and suggested solution! Though, on the
difference between behaviours in Isabelle 2015 and 2016: I definitely
did not have this problem with Isabelle 2015---which I've been using
almost daily until two days ago---as the inability to copy-paste
efficiently from the proof state panel is so annoying as to be
unmissable :(

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 12:57):

From: Makarius <makarius@sketis.net>
What is your window manager?

What is your Java Swing look-and-feel?

I've made a quick test with a standard installation of Ubuntu 14.04, with
Isabelle2016 using fresh defaults: no problem to copy from Output or State
panel -- using C+C or C+INSERT as usual.

It is also possible that old jEdit properties copied from Isabelle2015 or
Isabelle2016 cause problems. By default nothing is done in this respect,
and it is the responsibility of the user to do this carefully by hand.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:57):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I can only presume what Dominic is using, but I am using the standard Unity
setup that ships with Ubuntu 14.04.

As I mentioned in my response, it is in fact possible to copy text using C-C/C-V.
However, I would normally expect to be able to copy text using right-click copy.
This does not work as expected. If you try to right click, the selection is
immediately cancelled and nothing goes into the selection buffer.

- Gene Stark

view this post on Zulip Email Gateway (Aug 22 2022 at 12:57):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Indeed, I am using the standard Unity setup in Ubuntu, though I use the GDK
look and feel within Isabelle/jEdit. My experience differs slightly from
Eugene however in that I cannot reliably copy from the output pane using
Ctrl+C, or rather I have to press Ctrl+C multiple times to ensure that
whatever I select is really copied to the clipboard. From testing, there
appears to be nothing wrong with my keyboard (I have no trouble pressing
Ctrl+C to copy in any other application, and even copying within the jEdit
editor frame works as expected), so whatever problem it is is localised to
the output frame.

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 12:58):

From: Makarius <makarius@sketis.net>
There is a slight non-uniformity of the main jEdit text areas vs. addition
GUI components, like the Output, State, Info panels. In particular, the
latter don't have standard menu or keyboard actions of jEdit: only a
subset is imitated.

The copy operation in that case is a rather unexciting key event handler:
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2016/src/Tools/jEdit/src/pretty_text_area.scala#l233

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:58):

From: Makarius <makarius@sketis.net>
On Sat, 12 Mar 2016, Dominic Mulligan via Cl-isabelle-users wrote:

Indeed, I am using the standard Unity setup in Ubuntu, though I use the
GDK look and feel within Isabelle/jEdit. My experience differs slightly
from Eugene however in that I cannot reliably copy from the output pane
using Ctrl+C, or rather I have to press Ctrl+C multiple times to ensure
that whatever I select is really copied to the clipboard.

I have experimented with the GTK look-and-feel a bit on Ubuntu 14.04, and
still don't see any problems.

From the description, it could be also a problem caused by some X11 input
method. The Isabelle/jEdit says in the last chapter:

:black_small_square: ❙‹Problem:› Some Linux/X11 input methods such as IBus tend to
disrupt key event handling of Java/AWT/Swing.

❙‹Workaround:› Do not use X11 input methods. Note that environment
variable ▩‹XMODIFIERS› is reset by default within Isabelle settings

That text was written for Fedora Linux some years ago. The situation might
be slightly differently in Ubuntu, if special input methods are enabled.

Another potential source of problems is the Java version: Isabelle2015
uses Java 7, Isabelle2016 uses Java 8. In the bundled distribution, it is
located in contrib/jdk. You can rename
Isabelle2016/contrib/jdk/x86_64-linux to get it out of the way and put
Isabelle2015/contrib/jdk/x86_64-linux in its place (assuming this is 64bit
Linux). It is important to keep the rest unchanged, notably the content of
Isabelle2016/contrib/jdk/etc.

Makarius


Last updated: Apr 23 2024 at 08:19 UTC