Fix #1429 - Use basic-devtools module (#1430)

This MR brings in `$`, `$$`, and `$x` browsers devtools' utilities to our code so we can use these whenever we find it convenient.
This commit is contained in:
Andrea Giammarchi
2023-05-02 15:12:28 +02:00
committed by GitHub
parent 3a66be585f
commit 82613d016a
11 changed files with 47 additions and 27 deletions

View File

@@ -1,3 +1,5 @@
import { $ } from 'basic-devtools';
import { createSingularWarning, escape } from './utils';
export interface Stdio {
@@ -67,7 +69,7 @@ export class TargetedStdio implements Stdio {
*/
writeline_by_attribute(msg: string) {
const target_id = this.source_element.getAttribute(this.source_attribute);
const target = document.getElementById(target_id);
const target = $('#' + target_id, document);
if (target === null) {
// No matching ID
createSingularWarning(