The Isabelle/jEdit Prover IDE
- The original jEdit look-and-feel is generally preserved, although
some default properties have been changed to accommodate Isabelle
(e.g. the text area font).
- Formal Isabelle/Isar text is checked asynchronously while editing.
The user is in full command of the editor, and the prover refrains
from locking portions of the buffer etc.
- Prover feedback works via tooltips, syntax highlighting, colors,
boxes etc. based on semantic markup provided by Isabelle in the
background.
- Using the mouse together with the modifier key C
(CONTROL on Linux or Windows,
COMMAND on Mac OS) exposes additional information.
- Dockable panels (e.g. Output) are managed as independent
windows by jEdit, which also allows multiple instances.
Isabelle symbols and fonts
- Isabelle supports infinitely many symbols:
α, β, γ, …
∀, ∃, ∨, ∧, ⟶, ⟷, …
≤, ≥, ⊓, ⊔, …
ℵ, △, ∇, …
\<foo>, \<bar>, \<baz>, …
- There are some special control symbols to modify the style of a
single symbol:
⇩ subscript
⇧ superscript
⇣ subscript within identifier
⇡ superscript within identifier
❙ bold face
- A default mapping relates some Isabelle symbols to Unicode points
(see $ISABELLE_HOME/etc/symbols and $ISABELLE_HOME_USER/etc/symbols).
- The IsabelleText font ensures that Unicode points are actually
seen on the screen (or printer).
- Input methods:
- copy/paste from decoded source files
- copy/paste from prover output
- completion provided by Isabelle plugin, e.g.
name | abbreviation | symbol |
lambda | % | λ |
Rightarrow | => | ⇒ |
Longrightarrow | ==> | ⟹ |
And | !! | ⋀ |
equiv | == | ≡ |
forall | ! | ∀ |
exists | ? | ∃ |
longrightarrow | --> | ⟶ |
and | /\ | ∧ |
or | \/ | ∨ |
not | ~ | ¬ |
noteq | ~= | ≠ |
in | : | ∈ |
notin | ~: | ∉ |
sub | =_ | ⇩ |
sup | =^ | ⇧ |
isup | -_ | ⇣ |
isub | -^ | ⇡ |
bold | -. | ❙ |
- NOTE: The above abbreviations refer to the input method.
The logical notation provides ASCII alternatives that often
coincide, but deviate occasionally.
- NOTE: Generic jEdit abbreviations or plugins perform similar
source replacement operations; this works for Isabelle as long
as the Unicode sequences coincide with the symbol mapping.
Limitations and workrounds (January 2011)
- No way to start/stop prover or switch to a different logic.
Workaround: Change options and restart editor.
- Multiple theory buffers cannot depend on each other, imports are
resolved via the file-system.
Workaround: Save/reload files manually.
- No reclaiming of old/unused document versions in prover or
editor.
Workaround: Avoid large files; restart after a few hours of use.
- Incremental reparsing sometimes produces unexpected command
spans.
Workaround: Cut/paste larger parts or reload buffer.
- Command execution sometimes gets stuck (purple background).
Workaround: Force reparsing as above.
- Odd behavior of some diagnostic commands, notably those
starting external processes asynchronously
(e.g. thy_deps, sledgehammer).
Workaround: Avoid such commands.
- No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
loading external files.
- General lack of various conveniences known from Proof
General.