【发布时间】：2014-06-19 09:05:40
【问题描述】：
在Isabelle/HOL tutorial的第4.1.2节我们发现
按照惯例，只要 Proof General 的 X-Symbol 模式或 LaTeX 输出处于活动状态，就会启用“xsymbols”模式。
现在，随着 Proof General 的衰落，xsymbols 有什么相关性吗？
【问题讨论】：
【发布时间】：2014-06-19 09:05:40
【问题描述】：
xsymbols 模式仍然是 Isabelle/jEdit 中的默认模式。
虽然 Isabelle/jEdit 在编辑器中将符号呈现为 unicode，但在幕后内部表示仍使用xsymbol 编码。这可以通过在另一个编辑器中打开保存的理论文件来看到。例如文字：
lemma "a ∧ b ⟹ b ∧ a"
by simp
以xsymbols 编码保存到文件中：
lemma "a \<and> b \<Longrightarrow> b \<and> a"
by simp
jEdit 的 Isabelle 插件在与主 Isabelle 进程通信时执行与 unicode 之间的转换。 （如果你好奇的话，可以在Isabelle/etc/symbols看到翻译表。）
这样做的实际结果是，如果您正在定义符号，xsymbols 指的是所有 LaTeX、ProofGeneral 和 Isabelle/jEdit。
也许将来会有unicode 模式，取代内部的xsymbols 表示，但我们还没有。
【讨论】：
-
关于“unicode 模式”的猜测：这已在 1998 年被驳回，并被各种参考手册中记录的“Isabelle 符号”所取代。