CODEWITHSUNDEEP
jeditisabelleproof-general
davidg
davidg

Reputation: 6027

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

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

ProofGeneral rendering of assumptions

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

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?

Upvotes: 5

Views: 882

Answers (2)

Charlie Parker
Charlie Parker

Reputation: 5266

  1. Go into Plugins -> Plugin Options -> Isabelle -> General
  2. then type in brackets in the Print Mode field.
  3. Click Apply.
  4. Then close out of Isabelle and restart it.

You should have brackets around your hypotheses thereafter.

Upvotes: 2

davidg
davidg

Reputation: 6027

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

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

ISABELLE_JEDIT_OPTIONS="-m brackets"

This will result in jEdit displaying brackets like ProofGeneral:

jEdit rendering brackets

Upvotes: 8

Related Questions