如何在Isabelle/jEdit中显示假设周围的括号？
如何在Isabelle/jEdit中显示假设周围的括号？
提问于 2013-04-11 09:24:32
当伊莎贝尔在ProofGeneral中显示目标时，假设是用括号括起来的：
然而，在Isabelle/jEdit中，这似乎已更改为元隐含箭头：
虽然我理解前者有些不标准，但我发现它更容易阅读。有没有办法修改Isabelle/jEdit的行为，以旧的ProofGeneral样式打印出目标？
回答 2
Stack Overflow用户
回答已采纳
发布于 2013-04-11 09:24:32
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的括号：
Stack Overflow用户
发布于 2020-05-02 06:32:03
- 进入
Plugins -> Plugin Options -> Isabelle -> General - ，然后在Print Mode字段中键入
brackets。 - 单击Apply。
- 然后关闭Isabelle并重新启动。
在此之后，你应该用括号括起你的假设。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/15939265
复制相关文章
相似问题
腾讯云开发者
