Opened 17 years ago
Last modified 11 years ago
#24 closed defect
Replace current undo management with document-based undo mechanism — at Version 5
Reported by: | Owned by: | David Aspinall | |
---|---|---|---|
Priority: | blocker | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description (last modified by )
The current undo management code uses a long history of commands sent to the prover, then weeds through them to figure out which commands need undoing and how. This is tedious and will not support context switching. Currently there is no queue of undo commands but instead a thread is made for each undo command as one-by-one they are processed by the prover; this has very poor performance.
The document itself has exactly the information needed to calculate undo commands, based on the processed position. Because the document locks the processed text, this is expected to be accurate. We can calculate a queue of commands for undoing just as we do when processing commands.
This work has begun but amounts to a major reorganisation/extension of the document model. This ticket will be used to track progress.
Change History (5)
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
Milestone: | PG-Eclipse-1.0.7 → PG-Eclipse-1.0.6 |
---|---|
Status: | new → assigned |
comment:3 Changed 17 years ago by
Priority: | major → blocker |
---|
comment:4 Changed 17 years ago by
comment:5 Changed 16 years ago by
Description: | modified (diff) |
---|
Current status: most of this reorganisation is complete. Some small but crucial fixes were committed today for undoing theories properly.
Current status: see notes in #157