Opened 17 years ago
Last modified 11 years ago
#9 new defect
Fix history in output view
| Reported by: | anonymous | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description
History in output view (or browsing it) is garbled.
Change History (5)
comment:1 Changed 17 years ago by
| Component: | documentation → proofgeneral-eclipse |
|---|
comment:2 Changed 17 years ago by
comment:3 Changed 17 years ago by
| Milestone: | → PG-Eclipse-1.0.6 |
|---|
comment:4 Changed 17 years ago by
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
|---|
Note: See
TracTickets for help on using
tickets.
Ideally should make proof state output history rational (i.e. clear on open goal, move back but not extend for undo).
That's probably too much effort for now, but improving the history buttons would be good. We should always display the top of the history, and keep a flag saying whether to push when some new text arrives. Blank screens are never pushed, neither is interim output. This would work well with an addText method, if we had one, for good efficiency with large output delivered in chunks.
This work is in-progress.