Decorators not always updated
There are some cases when the decorators do not get updated to reflect the active script changing. These should be tracked down and fixed, presumably with further calls to (and possible rationalisation of) the method ProofScriptDocument.updateProperties()
.
Change History (9)
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
|
Description: |
modified (diff)
|
Description: |
modified (diff)
|
Summary: |
Decorator fixes and appearance improvements →
Decorators not always updated
|
Description: |
modified (diff)
|
Type: |
enhancement →
defect
|
Milestone: |
PG-Eclipse-1.0.7
|
Other decoration possibilities: