Sort completions by priority #6
Conversation
|
|
||
| client: LeanLSPClient = ctx.request_context.lifespan_context.client | ||
| completions = client.get_completions(rel_path, line - 1, column - 1) | ||
|
|
||
| lines = content.splitlines() | ||
| if line > 0 and line <= len(lines): |
There was a problem hiding this comment.
this part of the code is crap and might benefit from some rewriting. we're just trying to extract the previous words here.
|
Thanks! I will take this as a basis and do some reformatting on this PR. |
|
Not sure this was the best workflow but what do you think about this PR? |
|
thanks, looks legit, i should have credits now so lemme play with it |
|
I'm just curious what you are using Lean for, @gaearon? I was so pleasantly surprised to see your contribution here! |
|
Just for fun. I kind of started with NNG and then went through some of MIL, and now that Tao is working on Analysis companion, I got back into it since I really enjoyed doing exercises from this book before I even got into Lean. So now I'm working through those exercises. |
Attempts to implement #5 (comment).
Note:
It does look like a good starting point though, if you forgive the fiddly word boundary logic. This might be better done with a regex or something.