2011-09-28 09:16:26 -04:00
|
|
|
// -*- mode: js; js-indent-level: 4; indent-tabs-mode: nil -*-
|
2019-01-31 09:07:06 -05:00
|
|
|
/* exported WorkspaceSwitcherPopup */
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2019-02-08 22:21:36 -05:00
|
|
|
const { Clutter, GLib, GObject, Meta, St } = imports.gi;
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2012-04-14 08:40:30 -04:00
|
|
|
const Main = imports.ui.main;
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2019-08-01 19:13:10 -04:00
|
|
|
var ANIMATION_TIME = 100;
|
2017-07-18 13:47:27 -04:00
|
|
|
var DISPLAY_TIMEOUT = 600;
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2017-10-30 21:23:39 -04:00
|
|
|
var WorkspaceSwitcherPopupList = GObject.registerClass(
|
|
|
|
class WorkspaceSwitcherPopupList extends St.Widget {
|
2017-10-30 20:03:21 -04:00
|
|
|
_init() {
|
2017-10-30 21:23:39 -04:00
|
|
|
super._init({ style_class: 'workspace-switcher' });
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2010-06-09 13:09:48 -04:00
|
|
|
this._itemSpacing = 0;
|
2011-02-09 10:00:29 -05:00
|
|
|
this._childHeight = 0;
|
|
|
|
this._childWidth = 0;
|
2019-06-04 15:22:26 -04:00
|
|
|
this._orientation = global.workspace_manager.layout_rows == -1
|
|
|
|
? Clutter.Orientation.VERTICAL
|
|
|
|
: Clutter.Orientation.HORIZONTAL;
|
2010-02-16 16:34:57 -05:00
|
|
|
|
2018-07-15 17:00:07 -04:00
|
|
|
this.connect('style-changed', () => {
|
2019-01-29 14:36:54 -05:00
|
|
|
this._itemSpacing = this.get_theme_node().get_length('spacing');
|
2018-07-15 17:00:07 -04:00
|
|
|
});
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2019-01-31 09:08:10 -05:00
|
|
|
_getPreferredSizeForOrientation(_forSize) {
|
2013-01-28 00:09:12 -05:00
|
|
|
let workArea = Main.layoutManager.getWorkAreaForMonitor(Main.layoutManager.primaryIndex);
|
2018-07-15 17:00:07 -04:00
|
|
|
let themeNode = this.get_theme_node();
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
let availSize;
|
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL)
|
|
|
|
availSize = workArea.width - themeNode.get_horizontal_padding();
|
|
|
|
else
|
|
|
|
availSize = workArea.height - themeNode.get_vertical_padding();
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
let size = 0;
|
2018-07-15 17:00:07 -04:00
|
|
|
for (let child of this.get_children()) {
|
2019-02-01 08:41:55 -05:00
|
|
|
let [, childNaturalHeight] = child.get_preferred_height(-1);
|
2019-06-04 15:22:26 -04:00
|
|
|
let height = childNaturalHeight * workArea.width / workArea.height;
|
|
|
|
|
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL)
|
|
|
|
size += height * workArea.width / workArea.height;
|
|
|
|
else
|
|
|
|
size += height;
|
2010-06-09 13:09:48 -04:00
|
|
|
}
|
|
|
|
|
2018-01-03 02:55:38 -05:00
|
|
|
let workspaceManager = global.workspace_manager;
|
|
|
|
let spacing = this._itemSpacing * (workspaceManager.n_workspaces - 1);
|
2019-06-04 15:22:26 -04:00
|
|
|
size += spacing;
|
|
|
|
size = Math.min(size, availSize);
|
|
|
|
|
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL) {
|
|
|
|
this._childWidth = (size - spacing) / workspaceManager.n_workspaces;
|
|
|
|
return themeNode.adjust_preferred_width(size, size);
|
|
|
|
} else {
|
|
|
|
this._childHeight = (size - spacing) / workspaceManager.n_workspaces;
|
|
|
|
return themeNode.adjust_preferred_height(size, size);
|
|
|
|
}
|
|
|
|
}
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
_getSizeForOppositeOrientation() {
|
|
|
|
let workArea = Main.layoutManager.getWorkAreaForMonitor(Main.layoutManager.primaryIndex);
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL) {
|
|
|
|
this._childHeight = Math.round(this._childWidth * workArea.height / workArea.width);
|
|
|
|
return [this._childHeight, this._childHeight];
|
|
|
|
} else {
|
|
|
|
this._childWidth = Math.round(this._childHeight * workArea.width / workArea.height);
|
|
|
|
return [this._childWidth, this._childWidth];
|
|
|
|
}
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
vfunc_get_preferred_height(forWidth) {
|
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL)
|
|
|
|
return this._getSizeForOppositeOrientation();
|
|
|
|
else
|
|
|
|
return this._getPreferredSizeForOrientation(forWidth);
|
|
|
|
}
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
vfunc_get_preferred_width(forHeight) {
|
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL)
|
|
|
|
return this._getPreferredSizeForOrientation(forHeight);
|
|
|
|
else
|
|
|
|
return this._getSizeForOppositeOrientation();
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2020-05-09 15:30:26 -04:00
|
|
|
vfunc_allocate(box) {
|
|
|
|
this.set_allocation(box);
|
2018-07-15 17:00:07 -04:00
|
|
|
|
|
|
|
let themeNode = this.get_theme_node();
|
|
|
|
box = themeNode.get_content_box(box);
|
|
|
|
|
2010-06-09 13:09:48 -04:00
|
|
|
let childBox = new Clutter.ActorBox();
|
|
|
|
|
2019-06-04 15:22:26 -04:00
|
|
|
let rtl = this.text_direction == Clutter.TextDirection.RTL;
|
|
|
|
let x = rtl ? box.x2 - this._childWidth : box.x1;
|
2011-02-09 10:00:29 -05:00
|
|
|
let y = box.y1;
|
2018-07-15 17:00:07 -04:00
|
|
|
for (let child of this.get_children()) {
|
2019-06-04 15:22:26 -04:00
|
|
|
childBox.x1 = Math.round(x);
|
|
|
|
childBox.x2 = Math.round(x + this._childWidth);
|
|
|
|
childBox.y1 = Math.round(y);
|
2011-02-09 10:00:29 -05:00
|
|
|
childBox.y2 = Math.round(y + this._childHeight);
|
2019-06-04 15:22:26 -04:00
|
|
|
|
|
|
|
if (this._orientation == Clutter.Orientation.HORIZONTAL) {
|
|
|
|
if (rtl)
|
|
|
|
x -= this._childWidth + this._itemSpacing;
|
|
|
|
else
|
|
|
|
x += this._childWidth + this._itemSpacing;
|
|
|
|
} else {
|
|
|
|
y += this._childHeight + this._itemSpacing;
|
|
|
|
}
|
2020-05-09 15:30:26 -04:00
|
|
|
child.allocate(childBox);
|
2010-06-09 13:09:48 -04:00
|
|
|
}
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2018-07-15 17:00:07 -04:00
|
|
|
});
|
|
|
|
|
2017-10-30 21:23:39 -04:00
|
|
|
var WorkspaceSwitcherPopup = GObject.registerClass(
|
|
|
|
class WorkspaceSwitcherPopup extends St.Widget {
|
2018-07-15 17:00:07 -04:00
|
|
|
_init() {
|
2017-10-30 21:23:39 -04:00
|
|
|
super._init({ x: 0,
|
2018-07-15 17:00:07 -04:00
|
|
|
y: 0,
|
|
|
|
width: global.screen_width,
|
|
|
|
height: global.screen_height,
|
|
|
|
style_class: 'workspace-switcher-group' });
|
|
|
|
|
|
|
|
Main.uiGroup.add_actor(this);
|
|
|
|
|
|
|
|
this._timeoutId = 0;
|
|
|
|
|
|
|
|
this._container = new St.BoxLayout({ style_class: 'workspace-switcher-container' });
|
|
|
|
this.add_child(this._container);
|
|
|
|
|
|
|
|
this._list = new WorkspaceSwitcherPopupList();
|
|
|
|
this._container.add_child(this._list);
|
|
|
|
|
|
|
|
this._redisplay();
|
|
|
|
|
|
|
|
this.hide();
|
|
|
|
|
|
|
|
let workspaceManager = global.workspace_manager;
|
|
|
|
this._workspaceManagerSignals = [];
|
|
|
|
this._workspaceManagerSignals.push(workspaceManager.connect('workspace-added',
|
|
|
|
this._redisplay.bind(this)));
|
|
|
|
this._workspaceManagerSignals.push(workspaceManager.connect('workspace-removed',
|
|
|
|
this._redisplay.bind(this)));
|
|
|
|
|
|
|
|
this.connect('destroy', this._onDestroy.bind(this));
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-06-09 13:09:48 -04:00
|
|
|
|
2017-10-30 20:03:21 -04:00
|
|
|
_redisplay() {
|
2018-01-03 02:55:38 -05:00
|
|
|
let workspaceManager = global.workspace_manager;
|
|
|
|
|
2012-02-16 13:27:09 -05:00
|
|
|
this._list.destroy_all_children();
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2018-01-03 02:55:38 -05:00
|
|
|
for (let i = 0; i < workspaceManager.n_workspaces; i++) {
|
2010-02-12 17:52:15 -05:00
|
|
|
let indicator = null;
|
|
|
|
|
2019-01-29 14:36:54 -05:00
|
|
|
if (i == this._activeWorkspaceIndex && this._direction == Meta.MotionDirection.UP)
|
|
|
|
indicator = new St.Bin({ style_class: 'ws-switcher-active-up' });
|
|
|
|
else if (i == this._activeWorkspaceIndex && this._direction == Meta.MotionDirection.DOWN)
|
|
|
|
indicator = new St.Bin({ style_class: 'ws-switcher-active-down' });
|
2019-06-04 15:22:26 -04:00
|
|
|
else if (i == this._activeWorkspaceIndex && this._direction == Meta.MotionDirection.LEFT)
|
|
|
|
indicator = new St.Bin({ style_class: 'ws-switcher-active-left' });
|
|
|
|
else if (i == this._activeWorkspaceIndex && this._direction == Meta.MotionDirection.RIGHT)
|
|
|
|
indicator = new St.Bin({ style_class: 'ws-switcher-active-right' });
|
2019-01-29 14:36:54 -05:00
|
|
|
else
|
|
|
|
indicator = new St.Bin({ style_class: 'ws-switcher-box' });
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2019-01-29 14:36:54 -05:00
|
|
|
this._list.add_actor(indicator);
|
2010-02-12 17:52:15 -05:00
|
|
|
|
|
|
|
}
|
|
|
|
|
2013-01-28 00:09:12 -05:00
|
|
|
let workArea = Main.layoutManager.getWorkAreaForMonitor(Main.layoutManager.primaryIndex);
|
2019-02-01 08:41:55 -05:00
|
|
|
let [, containerNatHeight] = this._container.get_preferred_height(global.screen_width);
|
|
|
|
let [, containerNatWidth] = this._container.get_preferred_width(containerNatHeight);
|
2013-01-28 00:09:12 -05:00
|
|
|
this._container.x = workArea.x + Math.floor((workArea.width - containerNatWidth) / 2);
|
|
|
|
this._container.y = workArea.y + Math.floor((workArea.height - containerNatHeight) / 2);
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2017-10-30 20:03:21 -04:00
|
|
|
_show() {
|
2018-07-20 15:46:19 -04:00
|
|
|
this._container.ease({
|
|
|
|
opacity: 255,
|
|
|
|
duration: ANIMATION_TIME,
|
2019-08-20 17:43:54 -04:00
|
|
|
mode: Clutter.AnimationMode.EASE_OUT_QUAD,
|
2018-07-20 15:46:19 -04:00
|
|
|
});
|
2019-04-09 19:26:19 -04:00
|
|
|
this.show();
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2017-10-30 20:03:21 -04:00
|
|
|
display(direction, activeWorkspaceIndex) {
|
2012-06-27 15:13:32 -04:00
|
|
|
this._direction = direction;
|
|
|
|
this._activeWorkspaceIndex = activeWorkspaceIndex;
|
|
|
|
|
|
|
|
this._redisplay();
|
2010-02-12 17:52:15 -05:00
|
|
|
if (this._timeoutId != 0)
|
2019-08-19 14:50:33 -04:00
|
|
|
GLib.source_remove(this._timeoutId);
|
|
|
|
this._timeoutId = GLib.timeout_add(GLib.PRIORITY_DEFAULT, DISPLAY_TIMEOUT, this._onTimeout.bind(this));
|
2014-04-10 13:26:52 -04:00
|
|
|
GLib.Source.set_name_by_id(this._timeoutId, '[gnome-shell] this._onTimeout');
|
2010-02-12 17:52:15 -05:00
|
|
|
this._show();
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2010-02-12 17:52:15 -05:00
|
|
|
|
2017-10-30 20:03:21 -04:00
|
|
|
_onTimeout() {
|
2019-08-19 14:50:33 -04:00
|
|
|
GLib.source_remove(this._timeoutId);
|
2010-02-12 17:52:15 -05:00
|
|
|
this._timeoutId = 0;
|
2018-07-20 15:46:19 -04:00
|
|
|
this._container.ease({
|
|
|
|
opacity: 0.0,
|
|
|
|
duration: ANIMATION_TIME,
|
|
|
|
mode: Clutter.AnimationMode.EASE_OUT_QUAD,
|
2019-08-20 17:43:54 -04:00
|
|
|
onComplete: () => this.destroy(),
|
2018-07-20 15:46:19 -04:00
|
|
|
});
|
2013-11-28 19:45:39 -05:00
|
|
|
return GLib.SOURCE_REMOVE;
|
2017-10-30 21:23:39 -04:00
|
|
|
}
|
2012-06-27 15:13:32 -04:00
|
|
|
|
2018-07-15 17:00:07 -04:00
|
|
|
_onDestroy() {
|
2012-06-27 15:13:32 -04:00
|
|
|
if (this._timeoutId)
|
2019-08-19 14:50:33 -04:00
|
|
|
GLib.source_remove(this._timeoutId);
|
2012-06-27 15:13:32 -04:00
|
|
|
this._timeoutId = 0;
|
|
|
|
|
2018-01-03 02:55:38 -05:00
|
|
|
let workspaceManager = global.workspace_manager;
|
|
|
|
for (let i = 0; i < this._workspaceManagerSignals.length; i++)
|
|
|
|
workspaceManager.disconnect(this._workspaceManagerSignals[i]);
|
2012-06-27 15:13:32 -04:00
|
|
|
|
2018-07-15 17:00:07 -04:00
|
|
|
this._workspaceManagerSignals = [];
|
2010-02-12 17:52:15 -05:00
|
|
|
}
|
2011-11-20 12:56:27 -05:00
|
|
|
});
|