Add spaces after brackets

[metakunt]

One of the annoyances I had with mmj2 was that I had to play tokenizer myself.

It would be cool if I could write (ph -> ps) or (A+ B) as for very large nested brackets there is a lots of spaces I have to add manually. This would be a minor QOL improvement for me.

I can also add the feature myself but I don't know what the correct hooks for the lsp are. If you have any ideas please let me know.

[glacode]

Thank you for raising this issue. It's important to recognize that certain symbols, like (ph, can be valid Metamath symbols in some theories, so we must handle them carefully.

For example, (,) is a valid symbol in set.mm and should not be split into ( , ), which are three other valid symbols.

One potential approach could be: on ctrl+u , if a well-formed formula (wff) contains an invalid symbol, we could try a custom tokenizer to see if it resolves the issue. Additionally, we could implement code that attempts automatic bracket balancing.

Please note that I rarely write out a full wff directly. Instead, I usually "proof backward": I write a label and ctrl+u. Occasionally, I replace working variables, but I don't typically write long sequences of symbols.

This is why Yamma has a bias towards proving backwards. I spend more time implementing strategies to speed up backward proving because it's the technique I am most familiar with.

[metakunt]

Ah cool, thanks for the feedback. Yeah I thought about that. I also try to do prove backwards where it exists. Few points. I wanted to make it gated behind a feature flag so that you can enable it optionally.

First how would I implement a feature like that. I thought about finding all symbols with ( or ) and carefully checking if they exist as a token, if not it would put spaces in between them. Do I need to know about some lsp hooks for that?

Second regarding backwards proving and forwards proving. I would like to write some documentation so that we can bundle all the ideas that we have and share them so that newer contributors can have a "guide" how to use the tooling available. I think that having a vscode extension is more practical than using mmj2, even though I have so far only been using mmj2.

I think one hard thing about backwards proving that I have is sometimes with a more complicated theorem I know which pieces I need but I don't know how to piece them together. So I start proving forwards. But it is really good advise to get familiar with proving things backwards that I should seriously consider.

Well now that I found out how to get yamma to run I will try it and give you some more accurate feedback. Maybe the feature isn't necessary with backwards proving after all.

[glacode]

If the custom tokenization has to be applied when ctrl+u is invoked, this could be a hook

https://github.com/glacode/yamma/blob/683654637385212b5b4fedf28935e004799ad7e4/server/src/mmp/MmpProofTransformer.ts#L320

Please, notice that by writing (ph yamma cannot give you any further syntax suggestion, for the following tokens of that line (because the wff parser fails at that token)

If you instead want to apply changes "on the fly" (while the user is writing, without waiting for a ctrl+u ) then a good hook would be this

https://github.com/glacode/yamma/blob/683654637385212b5b4fedf28935e004799ad7e4/server/src/server.ts#L378

This code is run whenever the mmp file is changed, and I'm currently building a .mmp parse tree and raising all the Diagnostics. But I'm NOT changing the source file.

You should instead return a TextEdit that tokenizes the wrong symbol on the fly (but that's a big change w.r.t. the current approach)