Feature request: use goal count information printed at top of goals buffer in modeline

[cpitclaudel]

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.

[cpitclaudel]

Related: coq/coq#14999

[Matafou]

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?

[Matafou]

As you suggest we could show it in the goals buffer modeline of course. I suppose it is more intuitive.

[Matafou]

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...