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: