[isabelle-dev] print modes

[Makarius]

On Fri, 11 May 2012, Christian Sternagel wrote:

> You are right. However, if the "target" is a "newbie", it is often very 
> important to have it _exactly_ as it has to be typed (which does not 
> necessarily hold depending on syntax translations etc., even if the 
> print mode is "").

We are back to the historic mix of several slightly different things:

   * prover input syntax
   * prover output syntax
   * physical rendering of the text encoding of the prover in the front-end
   * input methods to produce something that the prover will digest

In Isabelle/jEdit (and the adjacent HTML output) things can be copy-pasted 
right now in most situations, even the sub-superscripts.  I've spent quite 
some efforts on all this.  If it does not work in Isabelle2012-RC, it is 
the proper time to point out the remaining problems now.


 	Makarius