jeditisabelleproof-general

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?


Solution

  • 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