is "proof state" view needed anymore?
the CurrentStateView? ("Proof State") doesn't seem to be useful -- only shows "proofstate" pgip messages, which don't seem to come back any more.
remove this view so as not to confuse users? (LatestOutputView? is much better.)
otherwise improve documentation (and use) of State view so that its purpose clear.
Change History (3)
| Description: |
modified (diff)
|
| Summary: |
reconcile "proof state" view for →
is "proof state" view needed anymore?
|
| Resolution: |
→ fixed
|
| Status: |
new →
closed
|
| Milestone: |
PG-Eclipse-1.0.6
|
Good idea to remove this, has been done now.
There would be some rationale in keeping it, for a "three pane" style of interaction (see existing PG Emacs). In that case, proof states are shown in one output window and diagnostics in another. But Isar output has confused this distinction and we are moving to a more document centred output anyway: we may see the current state in an annotation hover instead (see PGTextHover). But in that case, we will still need to distinguish prover command output from non-scripted diagnostic command output.