Fix #160745. Fix streaming output styling and duplicates. (#169792)

This commit is contained in:
Peng Lyu
2022-12-21 20:58:23 -08:00
committed by GitHub
parent ac5baecb46
commit 42814d18a7

View File

@@ -172,9 +172,17 @@ function renderStream(outputInfo: OutputItem, container: HTMLElement, error: boo
const outputElement = (prev.firstChild as HTMLElement | null);
if (outputElement && outputElement.getAttribute('output-mime-type') === outputInfo.mime) {
// same stream
const text = outputInfo.text();
const element = document.createElement('span');
// find child with same id
const existing = outputElement.querySelector(`[output-item-id="${outputInfo.id}"]`) as HTMLElement | null;
if (existing) {
clearContainer(existing);
}
const text = outputInfo.text();
const element = existing ?? document.createElement('span');
element.classList.add('output-stream');
element.setAttribute('output-item-id', outputInfo.id);
insertOutput(outputInfo.id, [text], ctx.settings.lineLimit, ctx.settings.outputScrolling, element);
outputElement.appendChild(element);
return;
@@ -183,6 +191,7 @@ function renderStream(outputInfo: OutputItem, container: HTMLElement, error: boo
const element = document.createElement('span');
element.classList.add('output-stream');
element.setAttribute('output-item-id', outputInfo.id);
const text = outputInfo.text();
insertOutput(outputInfo.id, [text], ctx.settings.lineLimit, ctx.settings.outputScrolling, element);