Как в Isabelle / jEdit заключить предположения в скобки?

Когда цели отображаются Изабель в ProofGeneral, предположения отображаются в скобках следующим образом:

ДоказательствоОбщая визуализация предположений

Однако в Isabelle / jEdit это, похоже, изменилось на стрелки мета-импликации:

jEdit рендеринг предположений

Хотя я понимаю, что первое несколько нестандартно, мне гораздо легче читать. Есть ли способ изменить поведение Isabelle / jEdit для печати целей в старом стиле ProofGeneral?


isabelle proof-general jedit
person davidg    schedule 11.04.2013    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Формат вывода Изабель определяется ее «режимами печати». В 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:

jEdit скобки рендеринга

person davidg    schedule 11.04.2013
comment
этот путь не существует в моем jedit Plugins > Plugin Options > Isabelle/General > Print Mode, не могли бы вы обновить свой ответ, пожалуйста? - person Charlie Parker; 02.05.2020
comment
этот путь также не существует ~/.isabelle/etc/settings - person Charlie Parker; 02.05.2020

arrow_upward
0
arrow_downward

  1. Войдите в Plugins -> Plugin Options -> Isabelle -> General
  2. затем введите brackets в поле «Режим печати».
  3. Щелкните Применить.
  4. Затем закройте Изабель и перезапустите ее.

После этого ваши гипотезы должны быть заключены в скобки.

person Charlie Parker    schedule 01.05.2020