Gripes about Eclipse (for PG Emacs users)

You've been an Emacs user proving theorems in Proof General for more years than you care to mention. Now you're wondering if you can really manage to switch to this new fangled IDE thing and whether it will be worth the effort. It's not going to be straightforward, there are some failings in Eclipse as well as some more stumbling points for Proof General.

please extend this with other issues: documenting them here may help result in something being done

Issues for Proof General

Lack of multiple fonts in text editors

At the moment we're not as good as X-Symbol in Emacs for semi-wysiwyg editing of mathematical input. The main stumbling points are:

• Lack of multiple font support in the Eclipse text editor -- prevents sub/superscript, mixing glyphs from different fonts
  (This certainly was the case a couple of years ago, I'm not sure if it's changed yet)

• Lack of good Unicode fonts that have enough mathematical gylphs.
  Hopefully this will change with the soon-to-be-released (honest) Stix fonts.

Future possibilities:

• Work on improved versions of the Eclipse text editor (or consider using another widget?)
• Collaborate with Texlipse on providing an X-Symbol replacement that uses Stix.
• Investigate other approaches: for example, using MathML formulae editors.
  

Opinion

this is an orthogonal approach, ordinary text editing of markup (with symbol support) should always be available.

Pet peeves: things you may miss in Eclipse

Argh! No kill ring!

I really miss the Emacs kill ring (M-y), don't you? If so, please vote for Eclipse bug 45848.