Opened 17 years ago
Last modified 11 years ago
#35 new enhancement
Implement Java PGIP abstraction, independently of Eclipse code
| Reported by: | Owned by: | David Aspinall | |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description
We should have a PGIP abstraction in Java which is used to represent PGIP messages, and marshall to and from XML. This can be separated into different pieces (for prover commands, display commands).
A possibility is to use validated XML directly, even using automatically generated code made by EMF.
For the time being, work has begun on building up a hand-crafted abstraction in ed.inf.proofgeneral.pgip.
Note: See
TracTickets for help on using
tickets.
Additional note from old sources:
Best to work on this gradually, refactoring main code as we go and testing carefully. Easiest starting points are new pieces of PGIP not yet covered by existing code (cf. Fatality, Location). To cope with preferences, ObjType? might be a next step. (See Isabelle's pgip_types.ML for all types).