ProofGeneral
Feature request: use goal count information printed at top of goals buffer in modeline
I won't have time to implement this, but it should be easy and it should provide a nice quality of life improvement.
Each goal buffer stars with a header line, like this:
1 focused subgoal
(shelved: 1) (ID 339)
width : Z
BW : Bitwidth width
…
It would be nice to move that info to the modeline, next to the buffer name (*goals*). We can change the "lighter" of the response mode to be a variable for that, and then update the variable when we update the response buffer.
This would save a bit of space, which is always nice with large Coq goals.
PG already shows the number of goals in the scripting buffer modeline. People hardly notice it I suppose. What exact display do you have in mind?
As you suggest we could show it in the goals buffer modeline of course. I suppose it is more intuitive.
Actually I have been thinking of enhancing further the coq/PG UI wrt to number of subgoals and also script parenthesizing ({ }) and bullets. Ideally I would like coq to print all subgoals together with the corresponding bullet imbrication :
n subgoals.
current goal:
- + * {
n,m:nat
H: ...
H0: ....
======
...
}
forall n m: Z, ...
- + * forall n:nat, ...
- + forall x:bool, ....
- + forall n:Z, ...
- forall n:nat, ...
I think this information could be of some help when dealing with large proofs. I am not sure how PG could relay it in a nice way though...