Search code examples
isabellejeditxemacs

Is xsymbols used in Isabelle/JEdit?

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?

Solution

  • 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:

    lemma "a ∧ b ⟹ b ∧ a"
  by simp

    is saved to a file as its xsymbols encoding:

    lemma "a \<and> b \<Longrightarrow> b \<and> a"
  by simp

    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 internal xsymbols representation, but we are not there yet.