#71 closed enhancement (fixed)
Add Error Decoration to documents; optimise Active Script Decoration
Reported by: | Graham Dutton | Owned by: | Graham Dutton |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | error decoration jdt marker |
Cc: |
Description (last modified by )
Decoration which annotates the current error/warning state is currently not generated.
It should take the form of:
- if (error markers present) decorate with ("JDT Error")
- else if (warning markers present) decorate with ("JDT Warning")
- else no decoration.
This should appear in the Proof Explorer (see #7), though this may be by inheritance from the Project Explorer.
One major obstacle to this is that triggering decoration updates seems to be difficult to do. There should be some mechanism for forcing label provider updates, as calling updateForEnablementChange()
is discouraged and severely sub-optimal (though at the scale it is being used, does not cause any major problems at present).
Fixing the problem above will also improve efficiency of the Active/Processed? Script decorator.
Change History (4)
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) |
---|---|
Owner: | changed from David Aspinall to Graham Dutton |
comment:3 Changed 16 years ago by
Description: | modified (diff) |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Error and Warning Decorators work correctly -- though, like Active Script decorators, not in Proof Explorer.
Updates are now done in an efficient, compliant manner -- though it's not guaranteed that they are done at every useful opportunity.
Closing - Decoration of Proof Explorer tracked by #7.