diff -r a319da4fbfb0 -r acc680ab6204 src/Tools/jEdit/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/README.html Wed Jun 08 22:06:05 2011 +0200
@@ -0,0 +1,137 @@
+
+
+
+
+
+
+Notes on the Isabelle/jEdit Prover IDE
+
+
+
+
+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>, …
+
+
+ - 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 | ~: | ∉ |
+
+
+
+
+
+ - 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.
+
+
+
+
+