|
@@ -70,18 +70,6 @@ const SIDEBAR_CLASS = 'jp-SideBar';
|
|
|
const CURRENT_CLASS = 'jp-mod-current';
|
|
|
|
|
|
|
|
|
-/**
|
|
|
- * The options for adding a widget to a side area of the shell.
|
|
|
- */
|
|
|
-export
|
|
|
-interface ISideAreaOptions {
|
|
|
- /**
|
|
|
- * The rank order of the widget among its siblings.
|
|
|
- */
|
|
|
- rank?: number;
|
|
|
-}
|
|
|
-
|
|
|
-
|
|
|
/**
|
|
|
* The application shell for JupyterLab.
|
|
|
*/
|
|
@@ -99,8 +87,8 @@ class ApplicationShell extends Widget {
|
|
|
let hboxPanel = this._hboxPanel = new BoxPanel();
|
|
|
let dockPanel = this._dockPanel = new DockPanel();
|
|
|
let hsplitPanel = this._hsplitPanel = new SplitPanel();
|
|
|
- let leftHandler = this._leftHandler = new SideBarHandler('left');
|
|
|
- let rightHandler = this._rightHandler = new SideBarHandler('right');
|
|
|
+ let leftHandler = this._leftHandler = new Private.SideBarHandler('left');
|
|
|
+ let rightHandler = this._rightHandler = new Private.SideBarHandler('right');
|
|
|
let rootLayout = new BoxLayout();
|
|
|
|
|
|
topPanel.id = 'jp-top-panel';
|
|
@@ -169,9 +157,6 @@ class ApplicationShell extends Widget {
|
|
|
|
|
|
/**
|
|
|
* The current widget in the shell's main area.
|
|
|
- *
|
|
|
- * #### Notes
|
|
|
- * This property is read-only.
|
|
|
*/
|
|
|
get currentWidget(): Widget {
|
|
|
return this._dockPanel.currentWidget;
|
|
@@ -211,7 +196,7 @@ class ApplicationShell extends Widget {
|
|
|
* #### Notes
|
|
|
* Widgets must have a unique `id` property, which will be used as the DOM id.
|
|
|
*/
|
|
|
- addToTopArea(widget: Widget, options: ISideAreaOptions = {}): void {
|
|
|
+ addToTopArea(widget: Widget, options: ApplicationShell.ISideAreaOptions = {}): void {
|
|
|
if (!widget.id) {
|
|
|
console.error('widgets added to app shell must have unique id property');
|
|
|
return;
|
|
@@ -226,7 +211,7 @@ class ApplicationShell extends Widget {
|
|
|
* #### Notes
|
|
|
* Widgets must have a unique `id` property, which will be used as the DOM id.
|
|
|
*/
|
|
|
- addToLeftArea(widget: Widget, options: ISideAreaOptions = {}): void {
|
|
|
+ addToLeftArea(widget: Widget, options: ApplicationShell.ISideAreaOptions = {}): void {
|
|
|
if (!widget.id) {
|
|
|
console.error('widgets added to app shell must have unique id property');
|
|
|
return;
|
|
@@ -241,7 +226,7 @@ class ApplicationShell extends Widget {
|
|
|
* #### Notes
|
|
|
* Widgets must have a unique `id` property, which will be used as the DOM id.
|
|
|
*/
|
|
|
- addToRightArea(widget: Widget, options: ISideAreaOptions = {}): void {
|
|
|
+ addToRightArea(widget: Widget, options: ApplicationShell.ISideAreaOptions = {}): void {
|
|
|
if (!widget.id) {
|
|
|
console.error('widgets added to app shell must have unique id property');
|
|
|
return;
|
|
@@ -304,7 +289,7 @@ class ApplicationShell extends Widget {
|
|
|
}
|
|
|
|
|
|
/**
|
|
|
- * Close all tracked widgets.
|
|
|
+ * Close all widgets in the main area.
|
|
|
*/
|
|
|
closeAll(): void {
|
|
|
each(toArray(this._dockPanel.widgets()), widget => { widget.close(); });
|
|
@@ -314,8 +299,8 @@ class ApplicationShell extends Widget {
|
|
|
private _hboxPanel: BoxPanel;
|
|
|
private _dockPanel: DockPanel;
|
|
|
private _hsplitPanel: SplitPanel;
|
|
|
- private _leftHandler: SideBarHandler;
|
|
|
- private _rightHandler: SideBarHandler;
|
|
|
+ private _leftHandler: Private.SideBarHandler;
|
|
|
+ private _rightHandler: Private.SideBarHandler;
|
|
|
}
|
|
|
|
|
|
|
|
@@ -324,172 +309,190 @@ defineSignal(ApplicationShell.prototype, 'currentChanged');
|
|
|
|
|
|
|
|
|
/**
|
|
|
- * A class which manages a side bar and related stacked panel.
|
|
|
+ * The namespace for `ApplicationShell` class statics.
|
|
|
*/
|
|
|
-class SideBarHandler {
|
|
|
- /**
|
|
|
- * Construct a new side bar handler.
|
|
|
- */
|
|
|
- constructor(side: string) {
|
|
|
- this._side = side;
|
|
|
- this._sideBar = new TabBar({
|
|
|
- insertBehavior: 'none',
|
|
|
- removeBehavior: 'none',
|
|
|
- allowDeselect: true
|
|
|
- });
|
|
|
- this._stackedPanel = new StackedPanel();
|
|
|
- this._sideBar.hide();
|
|
|
- this._stackedPanel.hide();
|
|
|
- this._sideBar.currentChanged.connect(this._onCurrentChanged, this);
|
|
|
- this._stackedPanel.widgetRemoved.connect(this._onWidgetRemoved, this);
|
|
|
- }
|
|
|
-
|
|
|
- /**
|
|
|
- * Get the tab bar managed by the handler.
|
|
|
- */
|
|
|
- get sideBar(): TabBar {
|
|
|
- return this._sideBar;
|
|
|
- }
|
|
|
-
|
|
|
+export
|
|
|
+namespace ApplicationShell {
|
|
|
/**
|
|
|
- * Get the stacked panel managed by the handler
|
|
|
+ * The options for adding a widget to a side area of the shell.
|
|
|
*/
|
|
|
- get stackedPanel(): StackedPanel {
|
|
|
- return this._stackedPanel;
|
|
|
+ export
|
|
|
+ interface ISideAreaOptions {
|
|
|
+ /**
|
|
|
+ * The rank order of the widget among its siblings.
|
|
|
+ */
|
|
|
+ rank?: number;
|
|
|
}
|
|
|
+}
|
|
|
|
|
|
- /**
|
|
|
- * Activate a widget residing in the side bar by ID.
|
|
|
- *
|
|
|
- * @param id - The widget's unique ID.
|
|
|
- */
|
|
|
- activate(id: string): void {
|
|
|
- let widget = this._findWidgetByID(id);
|
|
|
- if (widget) {
|
|
|
- this._sideBar.currentTitle = widget.title;
|
|
|
- widget.activate();
|
|
|
- }
|
|
|
- }
|
|
|
|
|
|
+namespace Private {
|
|
|
+ export
|
|
|
/**
|
|
|
- * Collapse the sidebar so no items are expanded.
|
|
|
+ * An object which holds a widget and its sort rank.
|
|
|
*/
|
|
|
- collapse(): void {
|
|
|
- this._sideBar.currentTitle = null;
|
|
|
- }
|
|
|
+ interface IRankItem {
|
|
|
+ /**
|
|
|
+ * The widget for the item.
|
|
|
+ */
|
|
|
+ widget: Widget;
|
|
|
|
|
|
- /**
|
|
|
- * Add a widget and its title to the stacked panel and side bar.
|
|
|
- *
|
|
|
- * If the widget is already added, it will be moved.
|
|
|
- */
|
|
|
- addWidget(widget: Widget, rank: number): void {
|
|
|
- widget.parent = null;
|
|
|
- widget.hide();
|
|
|
- let item = { widget, rank };
|
|
|
- let index = this._findInsertIndex(item);
|
|
|
- this._items.insert(index, item);
|
|
|
- this._stackedPanel.insertWidget(index, widget);
|
|
|
- this._sideBar.insertTab(index, widget.title);
|
|
|
- this._refreshVisibility();
|
|
|
+ /**
|
|
|
+ * The sort rank of the widget.
|
|
|
+ */
|
|
|
+ rank: number;
|
|
|
}
|
|
|
|
|
|
/**
|
|
|
- * Find the insertion index for a rank item.
|
|
|
+ * A less-than comparison function for side bar rank items.
|
|
|
*/
|
|
|
- private _findInsertIndex(item: Private.IRankItem): number {
|
|
|
- return upperBound(this._items, item, Private.itemCmp);
|
|
|
+ export
|
|
|
+ function itemCmp(first: IRankItem, second: IRankItem): number {
|
|
|
+ return first.rank - second.rank;
|
|
|
}
|
|
|
|
|
|
/**
|
|
|
- * Find the index of the item with the given widget, or `-1`.
|
|
|
+ * A class which manages a side bar and related stacked panel.
|
|
|
*/
|
|
|
- private _findWidgetIndex(widget: Widget): number {
|
|
|
- return findIndex(this._items, item => item.widget === widget);
|
|
|
- }
|
|
|
+ export
|
|
|
+ class SideBarHandler {
|
|
|
+ /**
|
|
|
+ * Construct a new side bar handler.
|
|
|
+ */
|
|
|
+ constructor(side: string) {
|
|
|
+ this._side = side;
|
|
|
+ this._sideBar = new TabBar({
|
|
|
+ insertBehavior: 'none',
|
|
|
+ removeBehavior: 'none',
|
|
|
+ allowDeselect: true
|
|
|
+ });
|
|
|
+ this._stackedPanel = new StackedPanel();
|
|
|
+ this._sideBar.hide();
|
|
|
+ this._stackedPanel.hide();
|
|
|
+ this._sideBar.currentChanged.connect(this._onCurrentChanged, this);
|
|
|
+ this._stackedPanel.widgetRemoved.connect(this._onWidgetRemoved, this);
|
|
|
+ }
|
|
|
|
|
|
- /**
|
|
|
- * Find the widget which owns the given title, or `null`.
|
|
|
- */
|
|
|
- private _findWidgetByTitle(title: Title): Widget {
|
|
|
- let item = find(this._items, value => value.widget.title === title);
|
|
|
- return item ? item.widget : null;
|
|
|
- }
|
|
|
+ /**
|
|
|
+ * Get the tab bar managed by the handler.
|
|
|
+ */
|
|
|
+ get sideBar(): TabBar {
|
|
|
+ return this._sideBar;
|
|
|
+ }
|
|
|
|
|
|
- /**
|
|
|
- * Find the widget with the given id, or `null`.
|
|
|
- */
|
|
|
- private _findWidgetByID(id: string): Widget {
|
|
|
- let item = find(this._items, value => value.widget.id === id);
|
|
|
- return item ? item.widget : null;
|
|
|
- }
|
|
|
+ /**
|
|
|
+ * Get the stacked panel managed by the handler
|
|
|
+ */
|
|
|
+ get stackedPanel(): StackedPanel {
|
|
|
+ return this._stackedPanel;
|
|
|
+ }
|
|
|
|
|
|
- /**
|
|
|
- * Refresh the visibility of the side bar and stacked panel.
|
|
|
- */
|
|
|
- private _refreshVisibility(): void {
|
|
|
- this._sideBar.setHidden(this._sideBar.titles.length === 0);
|
|
|
- this._stackedPanel.setHidden(this._sideBar.currentTitle === null);
|
|
|
- }
|
|
|
+ /**
|
|
|
+ * Activate a widget residing in the side bar by ID.
|
|
|
+ *
|
|
|
+ * @param id - The widget's unique ID.
|
|
|
+ */
|
|
|
+ activate(id: string): void {
|
|
|
+ let widget = this._findWidgetByID(id);
|
|
|
+ if (widget) {
|
|
|
+ this._sideBar.currentTitle = widget.title;
|
|
|
+ widget.activate();
|
|
|
+ }
|
|
|
+ }
|
|
|
|
|
|
- /**
|
|
|
- * Handle the `currentChanged` signal from the sidebar.
|
|
|
- */
|
|
|
- private _onCurrentChanged(sender: TabBar, args: TabBar.ICurrentChangedArgs): void {
|
|
|
- let oldWidget = this._findWidgetByTitle(args.previousTitle);
|
|
|
- let newWidget = this._findWidgetByTitle(args.currentTitle);
|
|
|
- if (oldWidget) {
|
|
|
- oldWidget.hide();
|
|
|
+ /**
|
|
|
+ * Collapse the sidebar so no items are expanded.
|
|
|
+ */
|
|
|
+ collapse(): void {
|
|
|
+ this._sideBar.currentTitle = null;
|
|
|
}
|
|
|
- if (newWidget) {
|
|
|
- newWidget.show();
|
|
|
+
|
|
|
+ /**
|
|
|
+ * Add a widget and its title to the stacked panel and side bar.
|
|
|
+ *
|
|
|
+ * If the widget is already added, it will be moved.
|
|
|
+ */
|
|
|
+ addWidget(widget: Widget, rank: number): void {
|
|
|
+ widget.parent = null;
|
|
|
+ widget.hide();
|
|
|
+ let item = { widget, rank };
|
|
|
+ let index = this._findInsertIndex(item);
|
|
|
+ this._items.insert(index, item);
|
|
|
+ this._stackedPanel.insertWidget(index, widget);
|
|
|
+ this._sideBar.insertTab(index, widget.title);
|
|
|
+ this._refreshVisibility();
|
|
|
}
|
|
|
- if (newWidget) {
|
|
|
- document.body.setAttribute(`data-${this._side}Area`, newWidget.id);
|
|
|
- } else {
|
|
|
- document.body.removeAttribute(`data-${this._side}Area`);
|
|
|
+
|
|
|
+ /**
|
|
|
+ * Find the insertion index for a rank item.
|
|
|
+ */
|
|
|
+ private _findInsertIndex(item: Private.IRankItem): number {
|
|
|
+ return upperBound(this._items, item, Private.itemCmp);
|
|
|
}
|
|
|
- this._refreshVisibility();
|
|
|
- }
|
|
|
|
|
|
- /*
|
|
|
- * Handle the `widgetRemoved` signal from the stacked panel.
|
|
|
- */
|
|
|
- private _onWidgetRemoved(sender: StackedPanel, widget: Widget): void {
|
|
|
- this._items.removeAt(this._findWidgetIndex(widget));
|
|
|
- this._sideBar.removeTab(widget.title);
|
|
|
- this._refreshVisibility();
|
|
|
- }
|
|
|
+ /**
|
|
|
+ * Find the index of the item with the given widget, or `-1`.
|
|
|
+ */
|
|
|
+ private _findWidgetIndex(widget: Widget): number {
|
|
|
+ return findIndex(this._items, item => item.widget === widget);
|
|
|
+ }
|
|
|
|
|
|
- private _side: string;
|
|
|
- private _sideBar: TabBar;
|
|
|
- private _stackedPanel: StackedPanel;
|
|
|
- private _items = new Vector<Private.IRankItem>();
|
|
|
-}
|
|
|
+ /**
|
|
|
+ * Find the widget which owns the given title, or `null`.
|
|
|
+ */
|
|
|
+ private _findWidgetByTitle(title: Title): Widget {
|
|
|
+ let item = find(this._items, value => value.widget.title === title);
|
|
|
+ return item ? item.widget : null;
|
|
|
+ }
|
|
|
|
|
|
+ /**
|
|
|
+ * Find the widget with the given id, or `null`.
|
|
|
+ */
|
|
|
+ private _findWidgetByID(id: string): Widget {
|
|
|
+ let item = find(this._items, value => value.widget.id === id);
|
|
|
+ return item ? item.widget : null;
|
|
|
+ }
|
|
|
|
|
|
-namespace Private {
|
|
|
- export
|
|
|
- /**
|
|
|
- * An object which holds a widget and its sort rank.
|
|
|
- */
|
|
|
- interface IRankItem {
|
|
|
/**
|
|
|
- * The widget for the item.
|
|
|
+ * Refresh the visibility of the side bar and stacked panel.
|
|
|
*/
|
|
|
- widget: Widget;
|
|
|
+ private _refreshVisibility(): void {
|
|
|
+ this._sideBar.setHidden(this._sideBar.titles.length === 0);
|
|
|
+ this._stackedPanel.setHidden(this._sideBar.currentTitle === null);
|
|
|
+ }
|
|
|
|
|
|
/**
|
|
|
- * The sort rank of the widget.
|
|
|
+ * Handle the `currentChanged` signal from the sidebar.
|
|
|
*/
|
|
|
- rank: number;
|
|
|
- }
|
|
|
+ private _onCurrentChanged(sender: TabBar, args: TabBar.ICurrentChangedArgs): void {
|
|
|
+ let oldWidget = this._findWidgetByTitle(args.previousTitle);
|
|
|
+ let newWidget = this._findWidgetByTitle(args.currentTitle);
|
|
|
+ if (oldWidget) {
|
|
|
+ oldWidget.hide();
|
|
|
+ }
|
|
|
+ if (newWidget) {
|
|
|
+ newWidget.show();
|
|
|
+ }
|
|
|
+ if (newWidget) {
|
|
|
+ document.body.setAttribute(`data-${this._side}Area`, newWidget.id);
|
|
|
+ } else {
|
|
|
+ document.body.removeAttribute(`data-${this._side}Area`);
|
|
|
+ }
|
|
|
+ this._refreshVisibility();
|
|
|
+ }
|
|
|
|
|
|
- /**
|
|
|
- * A less-than comparison function for side bar rank items.
|
|
|
- */
|
|
|
- export
|
|
|
- function itemCmp(first: IRankItem, second: IRankItem): number {
|
|
|
- return first.rank - second.rank;
|
|
|
+ /*
|
|
|
+ * Handle the `widgetRemoved` signal from the stacked panel.
|
|
|
+ */
|
|
|
+ private _onWidgetRemoved(sender: StackedPanel, widget: Widget): void {
|
|
|
+ this._items.removeAt(this._findWidgetIndex(widget));
|
|
|
+ this._sideBar.removeTab(widget.title);
|
|
|
+ this._refreshVisibility();
|
|
|
+ }
|
|
|
+
|
|
|
+ private _side: string;
|
|
|
+ private _sideBar: TabBar;
|
|
|
+ private _stackedPanel: StackedPanel;
|
|
|
+ private _items = new Vector<Private.IRankItem>();
|
|
|
}
|
|
|
}
|