Closed roshanjames closed 10 years ago
This is an interesting feature, but I am not sure how to get it right… I am thinking of defining a verbosity level for typing and completion commands, so that the editor can tell us the expected verbosity of the answer. @asmanur any opinion?
On dim. 18/août 2013 (00:57), def-lkb wrote:
This is an interesting feature, but I am not sure how to get it right… I am thinking of defining a verbosity level for typing and completion commands, so that the editor can tell us the expected verbosity of the answer. @asmanur any opinion?
Emacs implements a bit of it with C-c d (show-type-def) that runs show-type on the type of the expression. However we could have a command expand that would expand the type, and bind it perhaps to two C-c C-t.
How would you define "the verbosity" ? the number of expand step you can do ?
Perhaps we could also have a function that show every possible expansion of a type.
It may take a long time with rec-types :'…
Yes, verbosity would be defined as the number of expand step, and be incremented by one each time the user do C-c C-t. Showing every possible expansion is useful for typing, not completion. We can probably keep completion as it is and only make typing more verbose. Same for module sigs.
Implemented in current master. Merlin infers verbosity from repeated execution of the same command (if you type or complete the same thing, it will expand completion).
I think a regression error got introduced in master: Previously when I asked for the type for a sig, It would show some concrete type. In version git-3b0904 it shows the type of Intable and Floatable.S as just 'a.
This should be fixed in master.
When I examine the sig Intable, I see the following:
While this is correct, this is not very helpful. To see what an Intable really is, I have to type out "Core_kernel.Intable.S" and then hit C-c C-t on it. It would be helpful if I could follow such equality definitions of sigs, without having to type out the defined type. For example, maybe I could just hit C-c C-t a second time.