General plans for Proof General on Eclipse

Here are our plans for some next things to implement in ProofGeneralEclipse. For a higher-level view on our goals, see PGEclipseFutureIdeas.

For more details at a lower level and most up-to-date, please see information in trac.

Merge multiple branches and contributions to code

We need to amalgamate:

1. Ahsan's branch: updated Broker support, event and preference page improvements
2. Elina Timiriassova's GEF work, if useful/good enough
3. Fixes/contributions Alex Heneveld may have (standalone, features)

Improvements to existing code

• Add test suite infrastructure using JUnit
• Use latest PGIP features for syntax (keyword configuration, etc)
• Use PGIP features for content generation (objtypes)
• Try to get preferences table for prover created dynamically from PGIP (NB: probably need update button and then restart, otherwise Eclipse hacking)

More advanced extensions

• Handling multiple provers
• Refactoring and other high-level operations
• Interfacing to IsaPlanner
• Interfacing to HiProof browser
• Further visualisations