Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

Tweak the Loogle search implementation slightly in a few ways. #318

Closed Julian closed 9 months ago

Julian commented 9 months ago

There's probably a few small other things that can be tidied.

Julian commented 9 months ago

These are all quite minor I think, and mostly was a way to just poke at your code. Will give it a fresh look in the morning before merging, but @hargoniX if you have any comments feel free to lemme know!

Julian commented 9 months ago

I meant to check if Loogle ever returns names with newlines for any absurdly long one. Hopefully not but leaving a just in case note to check.

hargoniX commented 9 months ago

No I don't think it should do that but @nomeata should probably know the details on that? I'm a little surprised about the types with newlines as well, can you comment on that Joachim?

Apart from that I believe the changes look fine.

nomeata commented 9 months ago

I'm using some delaborator that I found, but plan to refine that anyways (more concise syntax where possible, maybe omitting some types or names…), I can try to avoid newlines then. but better be defensive - s/\n/ / doesn't hurt

Julian commented 9 months ago

Thanks both!