|
@@ -51,7 +51,6 @@ const inspector: JupyterFrontEndPlugin<IInspector> = {
|
|
const { commands, shell } = app;
|
|
const { commands, shell } = app;
|
|
const command = CommandIDs.open;
|
|
const command = CommandIDs.open;
|
|
const label = 'Contextual Help';
|
|
const label = 'Contextual Help';
|
|
- const title = 'Contextual Help';
|
|
|
|
const namespace = 'inspector';
|
|
const namespace = 'inspector';
|
|
const tracker = new WidgetTracker<MainAreaWidget<InspectorPanel>>({
|
|
const tracker = new WidgetTracker<MainAreaWidget<InspectorPanel>>({
|
|
namespace
|
|
namespace
|
|
@@ -63,7 +62,7 @@ const inspector: JupyterFrontEndPlugin<IInspector> = {
|
|
if (!inspector || inspector.isDisposed) {
|
|
if (!inspector || inspector.isDisposed) {
|
|
inspector = new MainAreaWidget({ content: new InspectorPanel() });
|
|
inspector = new MainAreaWidget({ content: new InspectorPanel() });
|
|
inspector.id = 'jp-inspector';
|
|
inspector.id = 'jp-inspector';
|
|
- inspector.title.label = title;
|
|
|
|
|
|
+ inspector.title.label = label;
|
|
void tracker.add(inspector);
|
|
void tracker.add(inspector);
|
|
source = source && !source.isDisposed ? source : null;
|
|
source = source && !source.isDisposed ? source : null;
|
|
inspector.content.source = source;
|
|
inspector.content.source = source;
|
|
@@ -83,7 +82,7 @@ const inspector: JupyterFrontEndPlugin<IInspector> = {
|
|
inspector.isDisposed ||
|
|
inspector.isDisposed ||
|
|
!inspector.isAttached ||
|
|
!inspector.isAttached ||
|
|
!inspector.isVisible,
|
|
!inspector.isVisible,
|
|
- label: args => (args.isLauncher ? title : label),
|
|
|
|
|
|
+ label: label;
|
|
iconClass: args =>
|
|
iconClass: args =>
|
|
args.isLauncher ? 'jp-MaterialIcon jp-InspectorIcon' : '',
|
|
args.isLauncher ? 'jp-MaterialIcon jp-InspectorIcon' : '',
|
|
execute: () => openInspector()
|
|
execute: () => openInspector()
|
|
@@ -91,7 +90,7 @@ const inspector: JupyterFrontEndPlugin<IInspector> = {
|
|
|
|
|
|
// Add command to UI where possible.
|
|
// Add command to UI where possible.
|
|
if (palette) {
|
|
if (palette) {
|
|
- palette.addItem({ command, category: title });
|
|
|
|
|
|
+ palette.addItem({ command, category: label });
|
|
}
|
|
}
|
|
if (launcher) {
|
|
if (launcher) {
|
|
launcher.add({ command, args: { isLauncher: true } });
|
|
launcher.add({ command, args: { isLauncher: true } });
|