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

Question

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

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

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

Answer 1

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

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

ISABELLE_JEDIT_OPTIONS="-m brackets"

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

Answer 2

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

此后，您的假设周围应该有括号。