"Select next unproven goal" and related commands work poorly
When executing why3 ide examples/logic/einstein.why
, we initially get the following tree:
- ../einstein.why
- Goals
+ G1
+ Wrong
+ G2
Pressing "ctrl+down" or choosing "select next unproven goal" select Wrong
, as expected. Then, pressing "down" selects Goals
instead of G2
. In other words, "select next unproven goal" has done only half the work, since the interface still believes the cursor is on einstein.why
, thus selecting Goals
when pressing "down".