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?

Accepted Answer

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:

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

Solution

Problem