diff -r 70a4c11cd79e -r 55b82b1417d1 src/Tools/jEdit/README.html --- a/src/Tools/jEdit/README.html Thu Feb 07 13:20:05 2013 +0100 +++ b/src/Tools/jEdit/README.html Sun Feb 10 14:57:00 2013 +0100 @@ -23,9 +23,9 @@

- Isabelle/jEdit is the flagship application of the PIDE - framework — it illustrates many of the ideas in a realistic - manner, ready to be used right now in Isabelle applications. + Isabelle/jEdit is the flagship application of the PIDE framework + — it is ready for small and large Isabelle applications, for + beginners and experts alike.

@@ -48,31 +48,40 @@

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).
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.
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 tooltips, syntax highlighting, colors, - boxes etc. based on semantic markup provided by Isabelle in the - background.
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 C -(CONTROL on Linux or Windows, - COMMAND on Mac OS X) exposes additional information.
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) are managed as independent - windows by jEdit, which also allows multiple instances.
Dockable panels (e.g. Output, Symbols) are managed as +independent windows by jEdit, which also allows multiple instances.
Formal output (tooltips etc.) may be explored recursively, using the +
Formal output (in popups etc.) may be explored recursively, using the same techniques as in the editor source buffer.
Prover process and source files are managed by the Isabelle/Scala on -the editor side. The prover experiences a mostly timeless and -stateless environment of formal document content.
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.

@@ -152,19 +161,27 @@ as the Unicode sequences coincide with the symbol mapping. -

NOTE: Raw unicode characters within prover source files +

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

Lack of dependency managed for auxiliary files that contribute +
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.

Workaround:

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.
Some Linux desktop environments with extreme animation effects + may disrupt Java 7 window placement and keyboard focus.
+ Workaround: Disable such effects.
The native MacOSX plugin for jEdit tends to be disruptive. It - might or might not improve the user experience, and is off by - default.
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.
Java 7 on MacOSX is officially supported on Lion and Mountain - Lion, but not Snow Leopard. It usually works on the latter, but - there might be some instabilities.
Java 7 on MacOSX 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.

@@ -197,11 +216,15 @@

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/

jEdit: GPL (with special cases)
http://www.jedit.org

Lobo/Cobra: GPL and LGPL
http://lobobrowser.org/

JFreeChart: LGPL
http://www.jfree.org

+ +

Lobo/Cobra: GPL and LGPL
http://lobobrowser.org