Когда цели отображаются Isabelle в ProofGeneral, предположения оказываются как имеющие скобки вокруг них, как так:Как отображать скобки вокруг предположений в Isabelle/jEdit?
В Isabelle/jEdit, однако, это, похоже, изменилась к мета-импликации стрелки:
в то время как я понимаю, бывший несколько нестандартным, я считаю, это намного легче читать. Есть ли способ изменить поведение Isabelle/jEdit для печати целей в старом стиле ProofGeneral?
Формат 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:
