addLineWidget(widget) was called twice with the same widget, which caused
inifite loop in ace editor
This commit is contained in:
Dmitry Vasilev
2023-07-11 21:51:46 +03:00
parent fc086e8c49
commit 3d9ea7a44b

View File

@@ -268,7 +268,7 @@ export class Editor {
content.appendChild(el('span', 'eval_error', stringify_for_header(error))) content.appendChild(el('span', 'eval_error', stringify_for_header(error)))
} }
this.widget = { const widget = this.widget = {
row, row,
fixedWidth: true, fixedWidth: true,
el: container, el: container,
@@ -276,8 +276,8 @@ export class Editor {
} }
const LineWidgets = require("ace/line_widgets").LineWidgets;
if (!session.widgetManager) { if (!session.widgetManager) {
const LineWidgets = require("ace/line_widgets").LineWidgets;
session.widgetManager = new LineWidgets(session); session.widgetManager = new LineWidgets(session);
session.widgetManager.attach(this.ace_editor); session.widgetManager.attach(this.ace_editor);
} }
@@ -287,7 +287,7 @@ export class Editor {
// which is async in ace_editor. Use setTimeout // which is async in ace_editor. Use setTimeout
setTimeout(() => { setTimeout(() => {
this.update_value_explorer_margin() this.update_value_explorer_margin()
session.widgetManager.addLineWidget(this.widget) session.widgetManager.addLineWidget(widget)
}, 0) }, 0)
} }