[isabelle-dev] copy-paste in Isabelle/jEdit

[Makarius]

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 
platform.

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 
http://www4.in.tum.de/~wenzelm/test/website/download.html ?


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 
expected.


> 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.


 	Makarius