()
| 2482 | } |
| 2483 | |
| 2484 | workspacesChanged() { |
| 2485 | let nWorkspaces = workspaceManager.n_workspaces; |
| 2486 | |
| 2487 | // Identifying destroyed workspaces is rather bothersome, |
| 2488 | // as it will for example report having windows, |
| 2489 | // but will crash when looking at the workspace index |
| 2490 | |
| 2491 | // Gather all indexed workspaces for easy comparison |
| 2492 | let workspaces = {}; |
| 2493 | for (let i = 0; i < nWorkspaces; i++) { |
| 2494 | let workspace = workspaceManager.get_workspace_by_index(i); |
| 2495 | workspaces[workspace] = true; |
| 2496 | if (this.spaceOf(workspace) === undefined) { |
| 2497 | this.addSpace(workspace); |
| 2498 | } |
| 2499 | } |
| 2500 | |
| 2501 | let nextUnusedWorkspaceIndex = nWorkspaces; |
| 2502 | for (let [, space] of this) { |
| 2503 | if (workspaces[space.workspace] !== true) { |
| 2504 | this.removeSpace(space); |
| 2505 | |
| 2506 | // Maps in javascript (and thus Spaces) remember insertion order |
| 2507 | // so the workspaces are sorted by index. The relative ordering |
| 2508 | // of the removed workspaces will thus be preserved when resurrected. |
| 2509 | space.settings.set_int('index', nextUnusedWorkspaceIndex); |
| 2510 | nextUnusedWorkspaceIndex++; |
| 2511 | } |
| 2512 | } |
| 2513 | |
| 2514 | // Ensure the live spaces have correct indices |
| 2515 | for (let [workspace, space] of this) { |
| 2516 | space.settings.set_int('index', workspace.index()); |
| 2517 | Meta.prefs_change_workspace_name(workspace.index(), space.name); |
| 2518 | } |
| 2519 | } |
| 2520 | |
| 2521 | /** |
| 2522 | * Return true if there are less-than-or-equal-to spaces than monitors. |
no test coverage detected