Closed Durbatuluk1701 closed 4 weeks ago
@gares Do you think this could possibly create unwanted side effects ?
I think that adding '
is a net win, I've seen quite some code naming stuff like foo'
.
The .
is a bit unclear to me. Nat.pl|us
is today considered as plus
, that is probably bad since it is more ambiguous than Nat.plus
. At the same time Na|t.plus
counts a Nat
. I don't know if, in that case, if the user expects to get info on the module Nat
or the addition. (I use |
for the caret position)
I think until we introduce some form of namespace it is a matter of deciding which is worse:
Nat.pl|us
Nat.plus
info on Na|t.plus
I think we can merge, but I did not test it.
Pushed a rework that should handle cases like:
lemma1_te|st
sandbox.mylem|ma
(also sand|box.mylemma
will have the same results, still not sure if that is desired behavior)
lem|ma'
(fully matches lemma'
and does not drop at single quotes)
Awesome ! I'll test and merge tomorrow ! Thanks !
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 !
This PR modified the
word_at_position
function 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