cleanup
ci/woodpecker/push/woodpecker Pipeline failed Details

This commit is contained in:
Malte Grosse 2024-02-05 15:41:23 +00:00
parent 92b4415b11
commit a5ca4ba0dd
1 changed files with 8 additions and 24 deletions

View File

@ -3,18 +3,16 @@ import {
JupyterFrontEndPlugin JupyterFrontEndPlugin
} from '@jupyterlab/application'; } from '@jupyterlab/application';
import { Widget } from '@lumino/widgets'; import { Widget } from '@lumino/widgets';
import { LogoAnnounce} from './images'; import { LogoAnnounce } from './images';
import { MainAreaWidget } from '@jupyterlab/apputils'; import { MainAreaWidget } from '@jupyterlab/apputils';
function generateContent(): string {
return 'Welcome to Sandbox Playground';
}
function createNode(): HTMLElement { function createNode(): HTMLElement {
let node = document.createElement('div'); let node = document.createElement('div');
node.className = "sandbox-announcement-container" node.className = "sandbox-announcement-container"
let content = document.createElement('div'); let content = document.createElement('div');
content.className = "sandbox-announcement-content" content.className = "sandbox-announcement-content"
let image = document.createElement('img'); let image = document.createElement('img');
image.src=LogoAnnounce; image.src = LogoAnnounce;
image.className = "sandbox-announcement-icon" image.className = "sandbox-announcement-icon"
content.appendChild(image); content.appendChild(image);
let text = document.createElement('h2'); let text = document.createElement('h2');
@ -36,34 +34,20 @@ const plugin: JupyterFrontEndPlugin<void> = {
const widget = new Widget(); const widget = new Widget();
widget.id = "sandbox-announce" widget.id = "sandbox-announce"
widget.addClass('sandbox-announcement-contentheader-widget'); widget.addClass('sandbox-announcement-contentheader-widget');
//widget.node.textContent = generateContent();
console.log(generateContent())
widget.node.appendChild(createNode()) widget.node.appendChild(createNode())
setInterval(() => { setInterval(() => {
const main = app.shell.currentWidget; const main = app.shell.currentWidget;
if (main !=null){
console.log(main);
}
if (main instanceof MainAreaWidget) { if (main instanceof MainAreaWidget) {
// if (main.title.label == 'Launcher'){
// console.log(main.title.label);
// }
let add = true; let add = true;
// and insert it into the header
main.contentHeader.widgets.forEach(function (w: Widget) { main.contentHeader.widgets.forEach(function (w: Widget) {
if (w.id=="sandbox-announce"){ if (w.id == "sandbox-announce") {
//w.dispose()
add = false add = false
} }
}); });
if (add){ if (add) {
console.log("add")
main.contentHeader.addWidget(widget); main.contentHeader.addWidget(widget);
} }
} }
}, 200); }, 200);