PG Eclipse: Summary of current Issues
This is a list of issues with PG Eclipse which may be show-stopper problems for users.
Fixing these will allow Proof General Eclipse to present a real alternative to the current Emacs Proof General.
Many issues and bugs have been fixed since September 2006 (interesting if you're using an older version of the plugin): see
PGEclipseFixesMade for outlines of these.
The most up-to-date bug and enhancement information (at a more technical level) is on
the Proof General trac. We welcome contributions and improvements
from others; please see
PGEclipseDevelopment.
Potential show stoppers
- Parsing proof scripts in Isabelle is unreliable and incomplete.
See http://proofgeneral.inf.ed.ac.uk/trac/ticket/83
- You may see warnings about unrecognised theory elements; some files may even fail to parse.
- It is hoped that this can be fixed in time for Isabelle2007.
- Symbol handling is not equivalent to X-Symbol in Emacs
- Many Unicode glyphs supported, but some X-Symbols may be missing
- Subscript or superscript aren't currently supported.
See http://proofgeneral.inf.ed.ac.uk/trac/ticket/80
- On the plus side, glyph/HTML output is extensible using HTML, Unicode and style sheets
- Efficiency and performance
- Eclipse itself requires more resources than Emacs
- There are some efficiency problems which require more work.
- Code and usability quality is being improved gradually; various intermittent bugs and usability flaws still remain.
Important note for users new to Eclipse
- Eclipse requires that all its files are stored in a Project in the Eclipse workspace
- Existing files must be imported (i.e. copied or linked) into the Eclipse workspace
- This does not impact on usability, but is important to understand, and is unlikely to change in future.