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

[Lawrence Paulson]

Cut and paste works much better with this version!

I still have to get to grips with a lot of very basic things, e.g. I gather some sort of auto complete mechanism exists…

Larry

On 20 Apr 2012, at 14:11, Makarius wrote:

> 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_______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev