[isabelle-dev] copy-paste in Isabelle/jEdit
makarius at sketis.net
Fri Apr 20 15:11:12 CEST 2012
On Wed, 18 Apr 2012, Christian Sternagel wrote:
> On 04/18/2012 03:42 PM, Lawrence Paulson wrote:
>> A further problem is you cannot cut and paste between the “proof"
>> window and the main window, so good luck creating any structured proofs
>> (unless you love typing lots of formal text and never make mistakes).
>> And on a Mac, the keyboard shortcuts are different from the usual.
> I don't get it. Copying and pasting between the output buffer and the
> main buffer works just fine for me (a bit odd is that you have to use
> Ctrl+C and Ctrl+V
Chris is a lucky Linux user who does not know all the snags of Apple's
Java 6, which was hardly maintained for many years and officially
deprecated last year. Until Java 8 is officially shipped by Oracle
(probably in 2013), one has to live with some limitations on that
Nonetheless, copy-paste between the Output panel (which is not a jEdit
buffer) and a jEdit buffer or any other GUI container should work, even
with regular COMMAND-C/V on Mac OS.
Larry could you try it again with the fully integrated test version from
Also note that the official specification of shortcomings and other
platform "features" in the Proper Session README says something like this:
The MacOSX plugin for jEdit disrupts regular C-X/C/V operations, e.g.
between the editor and the Console plugin, which is a standard swing
text box. Similar for search boxes etc.
This plugin is an optional add-on for jEdit. It changes a little over
time, and sometimes does good sometimes bad things. Few Mac users
contribute to jEdit significantly to keep things working smoothly. I've
developed a habit to disable all Mac specific configuration of jEdit,
apart from the main Look-and-feel, in order to make more things work as
> the linux-typical marking with mouse and middle click does not work
This vintage copy-paste feature from X11 is emulated specifically in jEdit
via the "Quick copy using middle mouse button". I've enabled this by
default for Isabelle/jEdit for convenience, but it is by construction
restricted to jEdit text buffers.
The Output panel is just another Swing component (Lobo HTML browser), not
a text buffer. This explains its slightly different copy-paste behaviour,
according to standard Java/Swing customs.
Lobo is OK for what is does right now, but I am waiting for Larry Ellison
to release the full HTML5 webpane for JVM 7 or 8 within the next year, or
so. Then we can do much more with the Output panel, apart from plain
copy-paste that already works better than for most PG/Emacs combinations
that I've seen over many years.
More information about the isabelle-dev