在Isabelle/HOL 教程的第 4.1.2 节中,我们发现
按照惯例,只要 Proof General 的 X-Symbol 模式或 LaTeX 输出处于活动状态,就会启用“xsymbols”模式。
现在,随着 Proof General 的衰落,xsymbols 有什么相关性吗?
在Isabelle/HOL 教程的第 4.1.2 节中,我们发现
按照惯例,只要 Proof General 的 X-Symbol 模式或 LaTeX 输出处于活动状态,就会启用“xsymbols”模式。
现在,随着 Proof General 的衰落,xsymbols 有什么相关性吗?
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
表示,但我们还没有。