Welcome to the Isabelle/jEdit Prover IDE

diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/README.html --- a/src/Tools/jEdit/README.html Sat Sep 21 16:08:17 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,237 +0,0 @@ - - - - - - - -Welcome to the Isabelle/jEdit Prover IDE - - - - -

- -

- PIDE is a framework for Prover IDEs based on the - Isabelle/Scala. It is built around a concept of - asynchronous document processing, which is supported - natively by the parallel proof engine that is implemented - in Isabelle/ML. -

- -

- Isabelle/jEdit is the main example application of the PIDE - framework — it is ready for small and large Isabelle - applications, for beginners and experts alike. -

- -

- Research and implementation of concepts around PIDE has started - around 2008 and was kindly supported by BMBF (http://www.bmbf.de), - Université Paris-Sud (http://www.u-psud.fr), Digiteo - (http://www.digiteo.fr), and ANR - (http://www.agence-nationale-recherche.fr). -

- - - -

The Isabelle/jEdit Prover IDE

- -

-Isabelle/jEdit consists of some plugins for the well-known jEdit text -editor framework (http://www.jedit.org), according to the following -principles. -

- -

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.
Prover feedback works via colors, boxes, squiggly underline, -hyperlinks, popup windows, icons, clickable output, all based on semantic -markup produced by Isabelle in the background.
Using the mouse together with the modifier key CONTROL (Linux, -Windows) or COMMAND (Mac OS X) exposes additional formal -content.
Dockable panels (e.g. Output, Symbols) are managed as -independent windows by jEdit, which also allows multiple instances.
Formal output (in popups etc.) may be explored recursively, using the -same techniques as in the editor source buffer.
The prover process and source files are managed on the editor side. The -prover operates on timeless and stateless document content via -Isabelle/Scala.
Plugin options of jEdit (for the Isabelle plugin) give access -to a selection of Isabelle/Scala options and its persistence preferences, -usually with immediate effect on the prover back-end or editor -front-end.
The logic image of the prover session may be specified within -Isabelle/jEdit, but this requires restart. The new image is provided -automatically by the Isabelle build process.

- - -

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: -

use the Symbols dockable
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	`=^`	⇧
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. -
NOTE: Raw Unicode characters within prover source files - should be restricted to informal parts, e.g. to write text in - non-latin alphabets. Mathematical symbols should be defined via the - official rendering tables. -
NOTE: Control symbols may be applied to a region of selected - text, either using the Symbols dockable or keyboard shortcuts.

- - -

Limitations and known problems

- -

Keyboard shortcuts C-PLUS and C-MINUS for adjusting the editor font - size depend on platform details and national keyboards.
- Workaround: Use numeric keypad or rebind keys in the jEdit Shortcuts - options dialog.
Lack of dependency management for auxiliary files that contribute - to a theory (e.g. ML_file).
- Workaround: Re-load files manually within the prover.
Odd behavior of some diagnostic commands with global - side-effects, like writing a physical - file.
- Workaround: Avoid such commands.
No way to delete document nodes from the overall collection of - theories.
- Workaround: Restart whole Isabelle/jEdit session in - worst-case situation.
Linux: some desktop environments with extreme animation effects - may disrupt Java 7 window placement and keyboard focus.
- Workaround: Disable such effects.
Linux: some X11 window managers that are not "re-parenting" - cause problems with additional windows opened by the Java VM. This - affects either historic or neo-minimalistic window managers like - awesome or xmonad.
- Workaround: Use regular re-parenting window manager.
Mac OS X: the native MacOSX plugin for jEdit tends to be - disruptive and is off by default. Enabling it might or might not - improve the user experience.
- Workaround: Disable MacOSX plugin.
Mac OS X: Java 7 is officially supported on Lion and Mountain Lion, - but not Snow Leopard. It usually works on the latter, although with a - small risk of instabilities.
- Workaround: Update to OS X Mountain Lion.

- - -

Licenses and home sites of contributing systems

- -

Isabelle: BSD-style
Poly/ML: LGPL
http://www.polyml.org
Scala: BSD-style
http://www.scala-lang.org
jEdit: GPL (with special cases)
http://www.jedit.org
JFreeChart: LGPL
http://www.jfree.org
Lobo/Cobra: GPL and LGPL
http://lobobrowser.org

- - -