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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
