Opened 17 years ago
Last modified 11 years ago
#21 new defect
Refactor to remove DummyDocElement
| Reported by: | Owned by: | David Aspinall | |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description (last modified by )
Refactor to remove the DummyDocElement atrocity. We should remove the overloading on document elements which are sent as commands to the prover (which should have their own type) and document elements which are really part of the document model. All the code should be aware of this distinction and not try to guess whether something is a command or document part.
Change History (3)
comment:1 Changed 17 years ago by
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
|---|
comment:2 Changed 17 years ago by
| Description: | modified (diff) |
|---|
comment:3 Changed 11 years ago by
| Milestone: | PG-Eclipse-1.0.7 |
|---|
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.0.7 deleted