Open DAIDE port on game loading and display on web

- Open DAIDE port on game loading too, and [web] Display DAIDE port on game title. 
- [server] Also delete backup game file when deleting game.
- [python]

Add optional parameter `server` to ServerGame constructor to init server game with a server as soon as it is possible.

Add field `daide_port` to Game for client games.

When creating game, register it on server before generating client games, so that DAIDE ports are known on client game generation.

Move DAIDE port opening into Server.add_new_game() and Server.get_game(), so that port is opened as soon as a new game is added or a game is loaded.

Move DAIDE port closing for specific game into Server.delete_game().

Add DAIDE port to client game field daide_port if known.

[web]

Display DAIDE port if available in game title on game page.

- [python] Display game ID in log when opening DAIDE port.
- [server] Close DAIDE port as soon as game is done.
- Update dependencies.

1 files changed, 14 insertions, 1 deletions

diff --git a/diplomacy/web/src/gui/pages/content_game.jsx b/diplomacy/web/src/gui/pages/content_game.jsx
index f1bc76c..7e7c7e9 100644
--- a/diplomacy/web/src/gui/pages/content_game.jsx
+++ b/diplomacy/web/src/gui/pages/content_game.jsx
@@ -71,6 +71,11 @@ const TABLE_POWER_VIEW = {
     wait: ['Waiting', 3]
 };
 
+const PRETTY_ROLES = {
+    [STRINGS.OMNISCIENT_TYPE]: 'Omnicient',
+    [STRINGS.OBSERVER_TYPE]: 'Observer'
+};
+
 export class ContentGame extends React.Component {
 
     constructor(props) {
@@ -157,8 +162,16 @@ export class ContentGame extends React.Component {
         this.vote = this.vote.bind(this);
     }
 
+    static prettyRole(role) {
+        if (PRETTY_ROLES.hasOwnProperty(role))
+            return PRETTY_ROLES[role];
+        return role;
+    }
+
     static gameTitle(game) {
-        let title = `${game.game_id} | ${game.phase} | ${game.status} | ${game.role} | ${game.map_name}`;
+        let title = `${game.game_id} | ${game.phase} | ${game.status} | ${ContentGame.prettyRole(game.role)} | ${game.map_name}`;
+        if (game.daide_port)
+            title += ` | DAIDE ${game.daide_port}`;
         const remainingTime = game.deadline_timer;
         if (remainingTime === undefined)
             title += ` (deadline: ${game.deadline} sec)`;