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

Question

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

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

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?

Answer 1

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:

Answer 2

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.