Opened 17 years ago
Last modified 11 years ago
#40 new enhancement
Implement document regions and annotations/markers for colouring
| Reported by: | Owned by: | David Aspinall | |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description
Use markers or annotations instead of coloured tokens. Fixes lots of mess with parsing and dummy document events, etc. Patch in progress, see StateMarkersEvents
branch (unfortunately performance/glitches may be an issue).
Intermediate point: use markers for contiguous regions in proof script, see #19. Separate patch also in progress (also has glitches).
Branch StateMarkersEvents also allows object states matching the PGIP edit model for different regions in the proof script. Before integrating this we should see how it fits in with Eclipse's existing notion of partitioning, and editing and re-parsing within partitions. Documents are allowed to have multiple overlapping partitionings, so we could use one for colouring processed regions, perhaps.
Milestone PG-Eclipse-1.1.0 deleted