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