Hi, While looking at the various usages of Map with Integer keys, I found ja.dict.UserDictionary with its lookup() method where there is a *TODO: can we avoid this treemap/toIndexArray?*
I could propose something, but I would like to know how much it is used, and if it is worth improving it. Thanks Bruno