mention tactic state in README

[lambdaofgod]

It might be useful to avoid confusion like in #62

[bustercopley]

Did you notice that the keybinding is already mentioned, in the "Key Bindings and Commands" section of README.txt?

[lambdaofgod]

Yes.

That's not the point though - as a first time user I didn't know what command should I run. I'd wager I'm not the only person who faced this problem.

[bustercopley]

A new user might not know what "show tactic state" means, either. Can you write something a bit longer, that will make the user think it is something they should try, and give them a clue about what will happen?

By the way, in VS Code, and in the video you linked in #62, "Tactic state" is a section heading, not the name of the tab/pane. In Emacs the buffer's name is *Lean Goals*, and the corresponding section heading is "Goals". I think we should talk about "showing the infoview".

[bustercopley]

Thank you for working on this!

[lambdaofgod]

While we're at it, maybe add a screenshot so people would see how it should look like? WDYT?

[bustercopley]

Maybe in a separate PR? I'm hesitant though, because the maintainers don't put much time into this repo and my guess is that easy, uncontroversial changes have a better chance of getting merged.

I don't know, maybe I'm being overcautious. @urkud?

[urkud]

I can review PRs on weekends and sometimes in the evening. Please ping me on zulip (mention or dm) when the pr is ready for review.