当Isabelle在ProofGeneral中显示目标时，假设将围绕它们的方括号呈现为:
但是，在Isabelle/jEdit中，这似乎已更改为元蕴含箭头:
虽然我知道前者有些不规范，但我发现它更容易阅读。有没有办法修改Isabelle/jEdit的行为以以旧的ProofGeneral样式打印目标？
最佳答案
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的括号:
关于jedit - 如何在Isabelle/jEdit中的假设周围显示方括号？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/15939265/