Improve symbols/character display: allow superscript, subscript (and maybe bold, italic, colours, ...)

[David Aspinall]

X-Symbol in Proof General Emacs allows superscripting and subscripting of parts of the input text. These are controlled by escape sequences, e.g.

• F<^bsub>x<^esub> produces F with x subscript, c.f. F_{x} in LaTeX
• F<^bsup>y<^esup> produces F with y super script, c.f. F^{y} in LaTeX

These are used moderately frequently in the Isabelle library theory files. So it is desirable to support this. We need to:

1. Support this markup in output text by altering the display style sheet. Should be easy.
2. Support this in the input editor.

The second point was impossible for a time because of limitations in the Eclipse StyledText widget, but these have now been addressed (see ​https://bugs.eclipse.org/bugs/show_bug.cgi?id=83405). To exploit this, we need to extend symbol handling to allow begin-end sequences, not just tokens; replacement operation must be allowed to affect the font style. This requires more effort and experimentation to get a robust solution for editing.

The output (and perhaps input) decoration should be standardised in PGML.

[David Aspinall]

Milestone PG-Eclipse-1.0.7 deleted