如何在Isabelle/jEdit中围绕假设显示括号？
dav*_*idg 4 jedit proof-general isabelle
当Isabelle在ProofGeneral中显示目标时,假设会围绕它们呈现括号,如下所示:
然而,在Isabelle/jEdit中,这似乎已经改为meta-implication箭头:
虽然我理解前者有点不标准,但我觉得它更容易阅读.有没有办法修改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一样的括号:
| 归档时间： |
|
| 查看次数： |
450 次 |
| 最近记录： |