The available options include:

• Isabelle/jEdit, the modified and preconfigured distribution of jEdit bundled with Isabelle installers
• Visual Studio Code with the Isabelle plugin (corresponding to the Isabelle version)

Deprecated or not supported:

• Isabelle/Eclipse
  • latest commit from 2013
  • states that support for Isabelle2013-1 is planned
• emacs with the Proof General plugin
  • official support for Isabelle has ended

This IDE feels old and clunky if one is used to more modern, cutting-edge solutions like JetBrains IntelliJ or Microsoft Visual Studio Code. However, considering all options, this seems to be the most promising one with the best user experience. Isabelle/jEdit comes ready for use, preconfigured, and bundled with the Isabelle installer.

TODO: verify that the following statements (changing symbol settings) also work for other editors than Isabelle/jEdit

As Isabelle uses many symbols of traditional mathematical notation (for instance ∧, the logical AND), internally represented by their ASCII names (e.g. \<and>), quick shortcuts for entering symbols are very convenient. Many shortcuts are provided by default (e.g. ==> for ⟹), however, some of them are also cumbersome to enter (e.g., /\ for ∧).

A symbol abbreviation that is a plain word, like ALL, is treated like a syntax keyword. Non-word abbreviations like --> are inserted more aggressively, except for single-character abbreviations like ! above.

-- jedit.pdf chapter 3.7.1.3 Isabelle symbols (p34)

Abbreviations can be added or removed by (creating and) editing the file $ISABELLE_USER_HOME/etc/symbols, following the syntax of $ISABELLE_HOME/etc/symbols.

Note: $ISABELLE_HOME is the location of the Isabelle installation (this is set by isabelle on startup and should not be modified, see system.pdf), and $ISABELLE_USER_HOME typically is $USER_HOME/.isabelle/Isabelle20xx. For Windows, $USER_HOME is %USERPROFILE%.

For instance, starting Isabelle the following symbols file (in the user settings directory) adds the abbreviations && for ∧ and || for ∨.

Note: the lines are copied and modified from the system version of symbols.

# add new abbreviation for logical and: &&
\<and>       code: 0x002227  group: logic  abbrev: /\  abbrev: &  abbrev: &&
# and for logical or: ||
\<or>        code: 0x002228  group: logic  abbrev: \/  abbrev: |  abbrev: ||

# remove || as abbreviation of these three symbols
# as only then || will be directly replaced
\<parallel>  code: 0x002225  group: punctuation
\<bar>       code: 0x0000a6  group: punctuation
\<bbar>      code: 0x002aff  group: punctuation

Does provide a less streamlined experience than Isabelle/jEdit, as the user has to manually install the IDE and extensions in addition to Isabelle itself (though this is subject to change).

Isabelle/VSCode started as an experiment (to learn from the VSCode platform) talk:isa-news (at ~22min) (see also talk:isa-vscode). It currently suffers from a few significant limitations (lacks Isabelle settings, no semantic highlighting in output, bad symbol handling, slower than jEdit).

The Isabelle distribution is planned to include a pre-configured VSCodium in the future (see Isabelle/VSCode as bundled application). This follows various improvements to Isabelle/VSCode made as part of a Bachelor thesis (see Denis Paluca: Isabelle/VSCode: Editor Improvements and Prover IDE integrations).

Install and configure extensions:

1. extension corresponding to the Isabelle version
   • for Isabelle20xx releases, use makarius.isabelle20xx,
   • for development builds, use makarius.isabelle
   • for a list of Isabelle/VSCode extensions, see extensions published by Makarius Wenzel.
2. install Prettify Symbols Mode
3. configure extensions
   1. in particular, set the isabelle.home variable:
      • enter settings via File > Preferences > Settings or Ctrl+,
      • enter isabelle.home in the search bar or navigate to Extensions > Isabelle > Isabelle: Home
      • enter the directory in which Isabelle is installed
   2. [optional] configure Prettify Symbols Mode
      • "prettifySymbolsMode.adjustCursorMovement": true
      • "prettifySymbolsMode.revealOn": "cursor" or "never"

• open an Isabelle/HOL .thy file
• show output
  • select View > Output (Ctrl+Shift+U)
  • there, select the Isabelle Output channel in the dropdown menu
• show the state
  • select View > Command Palette (Ctrl+Shift+P)
  • enter Isabelle: Show State
    • wait until the Isabelle backend has launched (will display a message), as executing show state before that will have no effect

Symbols, (like ⟹) are only visually inserted and the background representations (like \<Longrightarrow>) are hidden (unlike in jEdit where the ASCII representations are replaced by Unicode symbols in the editor buffer). This leads to strange behavior when trying to edit or remove such symbols.

The best way to cope with this seems to be to set the defaults for Prettify Symbols Mode as stated in the setup instructions. It does not seem to be possible to set these as Isabelle-specific since the Isabelle extension manages those.