Tracing goals in have and show

Stream: new members

[Brian Milnes]

I can't see (in either emacs or vs) the goal stack when using have and show. It works well when within begin and end.
When I move to the next lemma, it does not show "no goal". Nor does it show no goal after the lemma. This makes it a bit
harder to learn Lean that it should be. Is this intentional or a bug?

[Alex J. Best]

Can you give some screenshots /examples of where your cursor is and what you'd like to see?

[Alex J. Best]

I got into the habit of typing , (comma space) after everything to see the no goals after the last line

[Kevin Buzzard]

Can you confirm that you're using the leanprover-community version of Lean rather than the very old official Lean 3.4.2?