The font-lock setup misbehaves when started via menu

[Makarius]

The font-lock setup does not handle \<^sub> and \<^sub> properly if X-Symbol mode is enabled only later via the menu. For example, in Isabelle/HOL

  thm wf_trancl

displays \<^sup> verbatim. If the printed text is pasted into the source buffer it is shown properly as superscript. It also works as expected if X-Symbol is enabled right from the start, using option -x true.

[An Isabelle Developer]

This happens both for XEmacs and GNU Emacs; seems to be largely independent on version.

[Proof General Developer]

Yes, this is quite horrible. The mess of encodings used while constructing the Isabelle output, and the different possibilities with UTF-8/latin markup, together with the rusting of X-Symbol make it very hard to see what's going on. The behaviour is even different between output and goals buffers at the moment, although the code attempts to treat them similarly. Needs (hours of) further investigation, unfortunately.

[David Aspinall]

Fixed in proof-x-symbol.el 8.10 (proof-x-symbol-decode-region). Subscripts are handled via fontification in mule versions of Emacs, which was almost always by-passed entirely by the manual symbol decoding, without engaging font lock. Font lock can't be used for the output buffers because decoration is based on markup that is removed after fontifying (or never added).