如何在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的支架：