In the section 4.1.2 of the Isabelle/HOL tutorial we find
By convention, the mode of "xsymbols" is enabled whenever Proof General's X-Symbol mode or LaTeX output is active.
Now, with the fading of Proof General, is there any relevance of xsymbols?
xsymbols
mode is still the default in Isabelle/jEdit.While Isabelle/jEdit renders symbols in the editor as unicode, behind the scenes the internal representation is still using the
xsymbol
encoding. This can be seen by opening saved theory files up in another editor. For example, the text:is saved to a file as its
xsymbols
encoding:The Isabelle plugin to jEdit performs the translation to and from unicode as it communicates with the main Isabelle process. (The translation tables can be seen in
Isabelle/etc/symbols
, if you are curious.)The practical consequence of this is if your are defining notation,
xsymbols
refers to all of LaTeX, ProofGeneral and Isabelle/jEdit.Perhaps in the future there will be a
unicode
mode, replacing the internalxsymbols
representation, but we are not there yet.