Editing player names

[stengel]

Extensive form: The current naming of a player (with the animated triangle bouncing in from the right) is unintuitive, and does not behave well after the RETURN key. Clicking on the player IN THE GAME allows to change the name, just like move names. A corresponding small menu should pop up, like here:

which allows to select the player (as currently highlighted: 1: Alice) and change of the player name (text) and would also be the place to change the player colour (only a few choices please). The tickbox "change text only here" would mean the change is local to the current info set or node (can be implemented later, and requires corresponding field in file format). The same menu (minus the tickbox) would pop up when clicking a second time on the "select player" mode button. Also new is naming the chance player (currently none). A "rotate players" or "swap first two players" operation would also have its input here.

In the strategic form, no naming of players is currently possible. The player name should appear like Player 1: Alice and allowed to be clicked on for changing.