Access options in Utilities > Global Options

• Contents
• Editor
• Isabelle-specific
• Shortcuts
• Abbreviations

• Display line numbers
  • enable Global Options > jEdit > Gutter > Line numbers
• Open most recently visited directory in file browser at startup
  • select Most recently visited directory in Global Options > File System Browser > General

• select a session to load at start-up (if there are many slow imports in the project)
  • in Theories panel (docked on the right by default, alternatively activate using Plugins > Isabelle > Theories panel)
    or in Plugin Options > Isabelle > Logic
  • restart to apply
    • compiles at first launch and on changes to the imported libraries
    • significantly reduces start-up time on subsequent launches
  • HOL-Library is a good start, see the section on Session Images
• reduce Tooltip Delay (snappier Ctrl+Mouseover popup)
  • Plugin Options > Isabelle > Tooltip Delay
  • interferes with Ctrl+C when too low
    • when pressing while mouse is over some entity with a tooltip, the tooltip will open (because Ctrl is held) and the marked text will be out-of-focus
  • alternatively, use the Shortcut to manually open tooltips
• configure Code Completion
  • in Plugin Options > Isabelle > Completion
  • adjust delay, choose selection key (Tab and/or Enter)
• enable auto-tools (run tools without user interactions when cursor is over a goal)
  • Plugin Options > Isabelle > General > Automatically tried tools
  • recommended (quick and useful)
    • quickcheck (and/or nitpick) automatically check for counterexamples
    • solve_direct check if the current goal has already been proven somewhere else
  • not recommended (slow, may impact performance); use manually instead
    • methods is similar to try0
    • sledgehammer

Edit shortcuts in Global Options > jEdit > Shortcuts.

Some particularly useful actions with suggested shortcuts:

• Code Actions
  • Redo Ctrl+Shift+Z
  • Select all occurences of formal entity at caret F2 or Shift+F6
    • this is the closest thing to "smart rename" available in Isabelle/jEdit (cf. VSCode and IntelliJ)
  • Range Comment Ctrl+Shift+Divide
• Navigation
  • Back Alt+Left
  • Forward Alt+Right
  • Go to Previous Buffer Ctrl+Shift+Tab
  • Go to Next Buffer Ctrl+Tab
• Code Completion
  • Complete Isabelle text Ctrl+Space
• Utility
  • Show tooltip Ctrl+Q
  • Toggle continuous checking Pause

Note: when overwriting predefined shortcuts, Isabelle/jEdit will prompt for confirmation on next launch.

These are configured in $ISABELLE_USER_HOME/etc/symbols (see max_notes/isabelle#adjusting-abbreviations).
Note that jEdit provides built-in support for abbreviations (Global Options > jEdit > Abbreviations), however those are independent of the standard Isabelle symbol abbreviations (such as ==> being replaced by ⟹ immediately after typing it).

Some useful additions are presented here:

# all additional modifiers may be dropped, but `code: 0x...` should remain
# (for single character entries) as otherwise symbol replacement will be broken

# quick access to (single-character) sub-script and super-script
\<^sup> code: 0x0021e7 abbrev: ;;
\<^sub> code: 0x0021e9 abbrev: ,,

# abbreviations for pairs of brackets; sometimes more convenient than using the individual ones
# cartouches
\<open>\<close> abbrev: ``
# floor (`⌊ ⌋`) and ceiling (`⌈ ⌉`) brackets
\<lfloor>\<rfloor> abbrev: [_]
\<lceil>\<rceil> abbrev: [-]

# abbreviation `===` for `Pure.eq` (`≡`)
# omitting `abbrev: ==` will break this, as `==` will immediately be replaced by `\<rightleftharpoons>`
\<equiv> code: 0x002261 abbrev: == abbrev: ===