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

Question

当目标由伊莎贝尔在ProofGeneral显示，假设被渲染为具有身边括号像这样：

在伊莎贝尔/ 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的支架：