Opened 17 years ago
Last modified 11 years ago
#19 new defect
Use markers/positions for document processed and locked offsets
| Reported by: | Owned by: | David Aspinall | |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description
Instead of using fixed offsets, the positions should move with edits in the code. This would avoid problems if edits are enabled in the processed region.
Change History (4)
comment:1 Changed 17 years ago by
| Component: | documentation → proofgeneral-eclipse |
|---|---|
| Milestone: | → PG-Eclipse-1.0.6 |
comment:2 Changed 17 years ago by
comment:3 Changed 17 years ago by
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.1.0 |
|---|
Note: See
TracTickets for help on using
tickets.
This should fix the bug of missing tooltips(?), and the bug whereby markers are applied to the wrong locations.