fix: hover for period qualifiers and single quotes in names #899
Conversation
|
@gares Do you think this could possibly create unwanted side effects ? |
|
I think that adding The |
|
I think until we introduce some form of namespace it is a matter of deciding which is worse:
|
language-server/dm/rawDocument.ml
Outdated
| @@ -87,7 +87,7 @@ let range_of_loc raw loc = | |||
| } | |||
|
|
|||
| let word_at_position raw pos : string option = | |||
| let r = Str.regexp {|\([a-zA-Z_][a-zA-Z_0-9]*\)|} in | |||
| let r = Str.regexp {|\([a-zA-Z_.][a-zA-Z_0-9.']*\)|} in | |||
There was a problem hiding this comment.
I don't get why the . need to be part of the first character set.
The code below tries the regexp at a position and then goes back until it can.
There was a problem hiding this comment.
I originally didn't have it there but encountered the following issue since the code rolls back a single character at a time:
A case like Nat.pl|us it would roll back to Nat|.plus which then would no longer match unless the . was in first character set.
If you want I think a more robust way would be to roll back as far as possible to until you encounter [^a-zA-Z_0-9.'] then consume forward with {|\([a-zA-Z_][a-zA-Z_0-9.']*\)|}
There was a problem hiding this comment.
then there is an off by one error in the previous code
There was a problem hiding this comment.
Hmm yes I do think some more errors could creep up. If you hover something like lemma1_te|st I have a feeling it would stop at lemma|1_test since [0-9] does not appear in the first character set
There was a problem hiding this comment.
Just confirmed this is the case, will rework to be more robust
|
I think we can merge, but I did not test it. |
|
Pushed a rework that should handle cases like: |
|
Awesome ! I'll test and merge tomorrow ! Thanks ! |
This way if we hover over function, i.e. Module.fun|ction (the | representing the mouse) we get info on function and if we hover over Module, i.e. Mo|dule.function we get info on Module.
|
We did some experimenting with @gares and were able to get a solution to the Module.foo problem, I'll merge as soon as CI goes green ! Thanks again ! |
rtetley
changed the title
| let forward_reg = Str.regexp {|[^a-zA-Z_0-9']|} in | ||
| (* Search forwards ensuring that all characters are part of a well defined word. (Cannot start with [0-9'.] and cannot end with .)*) | ||
| let last_word_ind = Str.search_forward forward_reg raw.text start_ind in | ||
| let word = String.sub raw.text first_non_word_ind (last_word_ind - first_non_word_ind) in |
This PR modified the
word_at_positionfunction to allow for.and'to appear in names.This should fix #884
One note: It does allow for "words" to begin with a
., however it is just handled by providing no hover information since it would not be a legal name in Coq.Closes #884