hub icon indicating copy to clipboard operation
hub copied to clipboard

Add lean style math symbol completions

Open johannesCmayer opened this issue 1 year ago • 1 comments

Add math symbol completions based on the VScode lean extension.

johannesCmayer avatar Mar 23 '24 20:03 johannesCmayer

Hello! The CI found an error

Validating package: lean-symbols... Found 1 errors: Check: incoherent_path ->: package name mismatch in package lean-symbols: the path indicates that the name is lean-symbols, but the manifest calls it espanso-lean-symbols

Would you kindly fix it? It's almost there 😄

AucaCoyan avatar Apr 05 '24 01:04 AucaCoyan

I have now updated the package to incorporate all of the fixes. I will make another pull request because I actually regenerated all completions to the latest completions, and also removed all my custom modifications such that it is actually exactly the lean completions.

My main question is whether it makes sense to put the 30-line Python script that generates the completions in the package. It's not required, and it's not ever used, but it also seems like the natural place to put it.

johannesCmayer avatar Jun 16 '24 09:06 johannesCmayer

I have now updated the package to incorporate all of the fixes. I will make another pull request because I actually regenerated all completions to the latest completions, and also removed all my custom modifications such that it is actually exactly the lean completions.

My main question is whether it makes sense to put the 30-line Python script that generates the completions in the package. It's not required, and it's not ever used, but it also seems like the natural place to put it.

That seems reasonable. 30 lines isn't large, it may be of interest, and I suppose it would enable users to update the list if it changed, although you might update the package with a new version if that occurred. Include some explanatory text in your new README.md, perhaps.

smeech avatar Jun 16 '24 22:06 smeech