quint icon indicating copy to clipboard operation
quint copied to clipboard

VSCode plugin: Better support for showing things after "."

Open p-offtermatt opened this issue 1 year ago • 1 comments

One thing I think could be immensely useful is proper support for . in the VSCode plugin. When I type e.g.

currentState.

I would like a little box with all the field values (if record) and all the functions (say, that take a state as first parameter, which I'd liken to methods in an OO language) of the type that currentState is.

Not sure how much implementation effort it is, but imo it would be a big benefit in terms of usability. Right now, I often need to look through the spec to find whether there is a function that does what I am looking for, or make vague guesses that things that VSCode offers me in the autocompletion are functions related to the type I'm trying to use. This would make the VSCode autocompletions massively more useful

p-offtermatt avatar Jan 17 '24 08:01 p-offtermatt

For reference, we have some partial implementation of this by Thomas: https://github.com/informalsystems/quint/pull/1143

Should work for builtins, but is not consistent at all.

bugarela avatar Jan 17 '24 13:01 bugarela