isabelle - Isabelle/JEdit 中是否使用了 xsymbols？

Question

在Isabelle/HOL 教程的第 4.1.2 节中，我们发现

按照惯例，只要 Proof General 的 X-Symbol 模式或 LaTeX 输出处于活动状态，就会启用“xsymbols”模式。

现在，随着 Proof General 的衰落，xsymbols 有什么相关性吗？

Answer 1

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表示，但我们还没有。