Используются ли xsymbols в Isabelle/JEdit?

В разделе 4.1.2 учебника Изабель /HOL мы находим

По соглашению, режим "xsymbols" включается всякий раз, когда активен режим X-Symbol Proof General или выход LaTeX.

Теперь, с исчезновением Proof General, есть ли какое-то отношение к xsymbols?

Источник

1 ответ

Решение

xsymbols режим по-прежнему используется по умолчанию в Isabelle/jEdit.

В то время как Изабель / jEdit отображает символы в редакторе как юникод, за кулисами внутреннее представление все еще использует xsymbol кодирование. Это можно увидеть, открыв сохраненные файлы теории в другом редакторе. Например, текст:

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

сохраняется в файл как его xsymbols кодирование:

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

Плагин Isabelle для jEdit выполняет перевод в Unicode и обратно, поскольку он связывается с основным процессом Isabelle. (Таблицы перевода можно увидеть в Isabelle/etc/symbols, если вам любопытно.)

Практическое следствие этого, если вы определяете нотацию, xsymbols относится ко всем LaTeX, ProofGeneral и Isabelle/jEdit.

Возможно, в будущем будет unicode режим, заменяющий внутренний xsymbols представление, но мы еще не там.

Источник
Другие вопросы по тегам