如何在 Isabelle/jEdit 中的假设周围显示括号？

Question

当 Isabelle 在 ProofGeneral 中显示目标时，假设呈现为在它们周围有括号：

然而，在 Isabelle/jEdit 中，这似乎已更改为元含义箭头：

虽然我知道前者有些不标准，但我发现它更容易阅读。有没有办法修改 Isabelle/jEdit 的行为，以旧的 ProofGeneral 样式打印出目标？

Answer 1

Isabelle 呈现其输出的格式由 Isabelle 的“打印模式”决定。在 ProofGeneral 中，默认的 print_mode 包括 brackets 模式，它在假设周围呈现括号，而默认的 jEdit print_mode 包括 no_brackets，它的作用正好相反。

可以通过将Plugins > Plugin Options > Isabelle/General > Print Mode 设置为brackets 并重新启动jEdit、将-m brackets 添加到isabelle jedit 命令行或包含在~/.isabelle/etc/settings 文件中来更改打印模式：

ISABELLE_JEDIT_OPTIONS="-m brackets"

这将导致 jEdit 显示括号，如 ProofGeneral:

Answer 2

1. 进入Plugins -> Plugin Options -> Isabelle -> General
2. 然后在打印模式字段中输入brackets。
3. 点击应用。
4. 然后关闭 Isabelle 并重新启动它。

之后你的假设应该有括号。