[isabelle-dev] print modes

[Makarius]

On Fri, 11 May 2012, Lawrence Paulson wrote:

> I disagree. People frequently e-mail problems to one another. Of course, 
> the ability to paste readable Unicode symbols would be even better, but 
> that's surely too much to ask right now.

Part of the hidden context of this thread is the front-end you are using.

Some years ago, when the Proof General replacement project was started, 
Johannes Hölzl was one of the early students working on it.  He asked 
about the main new features to be supported, and my spontaneous answer 
was: copy-and-paste.

It is a long-standing running gag of Proof General / Emacs that it has its 
own peculiar ideas what copy-paste means.  In Isabelle/jEdit it should 
work most of the time, and the cases where it does not are boundary 
situations, not the default as under the old regime.


 	Makarius