Decorator fixes and appearance improvements
— at Version 5
- Decorator icons should be improved: make them smaller.
- There are some cases when the decorators do not get updated to reflect the active script changing. These should be tracked down and fixed. The failures may be related to recent changes in
ProofScriptDocument.java
which calls a method to update them; perhaps that method should be called in more places now.
Change History (5)
Summary: |
→ added more use-case suggestions
|
Description: |
modified (diff)
|
Summary: |
added more use-case suggestions →
Decorator fixes
|
Type: |
defect →
enhancement
|
Summary: |
Decorator fixes →
Decorator fixes and appearance improvements
|
Milestone: |
PG-Eclipse-1.0.6 →
PG-Eclipse-1.0.7
|
Description: |
modified (diff)
|
Owner: |
changed from David Aspinall to Graham Dutton
|
Other decoration possibilities: