blocks|key|2794522|text|Isabelle呈现其输出的格式由Isabelle的“打印模式”决定。在ProofGeneral中，默认的print_mode包括brackets模式，该模式在假设周围呈现括号，而默认的jEdit+print_mode包括no_brackets，后者执行相反的操作。|type|unstyled|depth|inlineStyleRanges|offset|length|style|CODE|entityRanges|data|2794523|可以通过将Plugins+>+Plugin+Options+>+Isabelle/General+>+Print+Mode设置为brackets并重新启动jEdit来更改打印模式，也可以通过将-m+brackets添加到isabelle+jedit命令行来更改打印模式，也可以通过在~/.isabelle/etc/settings文件中包含以下内容来更改打印模式：|2794524|ISABELLE_JEDIT_OPTIONS="-m+brackets"|code-block|syntax|javascript|2794525|这将导致jEdit显示类似于ProofGeneral的括号：|2794526|​|2794527|📷|atomic|2794528|2794529|entityMap|0|IMAGE|mutability|IMMUTABLE|imageUrl|https://ask.qcloudimg.com/http-save/yehe-900000/f0770b5c2cac2c4b2d8aa1a02e07e637.png|imageAlt^0|1H|A|1T|8|2R|A|33|B|0|5|1K|1S|8|2O|B|32|E|3X|O|0|0|0|0|0|1|0|0|0^^$0|@$1|2|3|4|5|6|7|13|8|@$9|14|A|15|B|C]|$9|16|A|17|B|C]|$9|18|A|19|B|C]|$9|1A|A|1B|B|C]]|D|@]|E|$]]|$1|F|3|G|5|6|7|1C|8|@$9|1D|A|1E|B|C]|$9|1F|A|1G|B|C]|$9|1H|A|1I|B|C]|$9|1J|A|1K|B|C]|$9|1L|A|1M|B|C]]|D|@]|E|$]]|$1|H|3|I|5|J|7|1N|8|@]|D|@]|E|$K|L]]|$1|M|3|N|5|6|7|1O|8|@]|D|@]|E|$]]|$1|O|3|P|5|6|7|1P|8|@]|D|@]|E|$]]|$1|Q|3|R|5|S|7|1Q|8|@]|D|@$9|1R|A|1S|1|1T]]|E|$]]|$1|T|3|P|5|6|7|1U|8|@]|D|@]|E|$]]|$1|U|3|-4|5|6|7|1V|8|@]|D|@]|E|$]]]|V|$W|$5|X|Y|Z|E|$10|11|12|-4]]]]

The format Isabelle renders its output is determined by Isabelle's "print modes". In ProofGeneral, the default <code>print_mode</code> includes the <code>brackets</code> mode, which renders brackets around assumptions, while the default jEdit <code>print_mode</code> includes <code>no_brackets</code>, which does the opposite.

The print mode can be changed either by setting <code>Plugins &gt; Plugin Options &gt; Isabelle/General &gt; Print Mode</code> to <code>brackets</code> and restarting jEdit, by adding <code>-m brackets</code> to the <code>isabelle jedit</code> command line, or by including in your <code>~/.isabelle/etc/settings</code> file:

<pre><code>ISABELLE_JEDIT_OPTIONS="-m brackets"
</code></pre>

This will result in jEdit displaying brackets like ProofGeneral:

<img src="https://i.stack.imgur.com/JNY4M.png" alt="jEdit rendering brackets">

blocks|key|17734|text|type|unstyled|depth|inlineStyleRanges|entityRanges|data|17735|进入Plugins+->+Plugin+Options+->+Isabelle+->+General+|ordered-list-item|offset|length|style|CODE|17736|，然后在Print+Mode字段中键入brackets。|17737|单击Apply。|17738|然后关闭Isabelle并重新启动。|17739|17740|在此之后，你应该用括号括起你的假设。|17741|entityMap^0|0|2|1C|0|J|8|0|0|0|0|0^^$0|@$1|2|3|-4|4|5|6|S|7|@]|8|@]|9|$]]|$1|A|3|B|4|C|6|T|7|@$D|U|E|V|F|G]]|8|@]|9|$]]|$1|H|3|I|4|C|6|W|7|@$D|X|E|Y|F|G]]|8|@]|9|$]]|$1|J|3|K|4|C|6|Z|7|@]|8|@]|9|$]]|$1|L|3|M|4|C|6|10|7|@]|8|@]|9|$]]|$1|N|3|-4|4|5|6|11|7|@]|8|@]|9|$]]|$1|O|3|P|4|5|6|12|7|@]|8|@]|9|$]]|$1|Q|3|-4|4|5|6|13|7|@]|8|@]|9|$]]]|R|$]]

<ol>
<li>Go into <code>Plugins -&gt; Plugin Options -&gt; Isabelle -&gt; General</code> </li>
<li>then type in <code>brackets</code> in the Print Mode field. </li>
<li>Click Apply.</li>
<li>Then close out of Isabelle and restart it. </li>
</ol>

You should have brackets around your hypotheses thereafter.

When goals are displayed by Isabelle in ProofGeneral, assumptions are rendered as having brackets around them as so:

<img src="https://i.stack.imgur.com/4tOP6.png" alt="ProofGeneral rendering of assumptions">

In Isabelle/jEdit, however, this seems to have changed to meta-implication arrows:

<img src="https://i.stack.imgur.com/5Dbhp.png" alt="jEdit rendering of assumptions">

While I understand the former is somewhat non-standard, I find it much easier to read. Is there a way to modify the behaviour of Isabelle/jEdit to print out goals in the old ProofGeneral style?

How do I display brackets around assumptions in Isabelle/jEdit?

翻译质量差，导致语言生硬或混乱。

没有提供实际的解决方法或示例。

解答不清晰，无法理解或解决问题。

页面排版不美观，阅读体验差。

文章

问答

视频

学习中心

腾讯云实验室

直播

竞赛

腾讯云代码分析专区

腾讯iOA零信任安全管理系统专区

腾讯云架构师技术同盟交流圈

腾讯云数据库专区

腾讯云顾问专区

腾讯云原生专区

腾讯混元专区

腾讯云TCE专区

腾讯云Lighthouse专区

腾讯云HAI专区

腾讯云Edgeone专区

腾讯云存储专区

腾讯云智能专区

腾讯轻联专区 

腾讯云开发专区

TAPD专区

腾讯轻量云游戏服专区

腾讯云最具价值专家

腾讯云架构师技术同盟

腾讯云创作之星

腾讯云开发者先锋

腾讯云代码助手

云原生构建

TAPD 敏捷项目管理

Cloud Studio

SDK中心

API中心

命令行工具

涵盖代码开发、场景应用、自动测试全流程，助你从零构建专属AI助手

一站式MCP教程库，解锁AI应用新玩法

当伊莎贝尔在ProofGeneral中显示目标时，假设是用括号括起来的：​​然而，在Isabelle/jEdit中，这似乎已更改为元隐含箭头：​​虽然我理解前者有些不标准，但我发现它更容易阅读。有没有办法修改Isabelle/jEdit的行为，以旧的ProofGeneral样式打印出目标？

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

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

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