Allow mapping from a Menu selection to arbitrary values, not just an integer

[KronosTheLate]

The current menus return an integer that represents the elected element(s). It would be nice to supply an optional vector of values that should be mapped to. This could simplify the mapping from selection to some other value, by packing into the Menu, where it feels like it would belong. This vector of "values mapped to" would then default to range(1, length(my_menu.titles), preserving the old behavior. To be more concrete, I imagine removing the field n_titles, which I presume is used to create such a range internally, and add a field values. Perhaps it would also make sense to change the name of titles to keys, to intuitively connect the keys and values fields.

As this change would only alter internal fields, I do not believe it is breaking according to SemVer.

Do you agree that this would be valuable? The current solution to this problem would be to take the return value and index another array, which would need it's own variable. It seems sensible to me to pack that common usage neatly in the Menu itself, where it seems to fit nicely. This is also how it is done in the drop-down selection element from PlutoUI, which I believe bases itself on some Mozilla internals.

[FedeClaudi]

Hey,

Yeah that makes a lot of sense.

The current solution to this problem would be to take the return value and index another array

That's what I had as I thought it would make it more flexible in terms of how the use selection is handled, but as you say that can still be the default behavior.

It seems like a great idea, do you want to send a PR?

[KronosTheLate]

I am not sure how, and I have a few other rods in the fire, so this will not be a priority for me for a long time. If you think you know how to do this without it taking too much effort from you, feel very free to give it a go, and I can contribute by testing it.

[FedeClaudi]

Sounds good!