Input and output character encodings can now be set

2022-09-02 12:56:04 +01:00
parent 7c8a185a3d
commit e93aa42697
15 changed files with 482 additions and 423 deletions
@@ -65,9 +65,11 @@ class HTMLWidget extends WidgetType {
     */
    replaceControlChars(textNode) {
        const val = escapeControlChars(textNode.nodeValue, true, this.view.state.lineBreak);
-        const node = document.createElement("null");
-        node.innerHTML = val;
-        textNode.parentNode.replaceChild(node, textNode);
+        if (val.length !== textNode.nodeValue.length) {
+            const node = document.createElement("span");
+            node.innerHTML = val;
+            textNode.parentNode.replaceChild(node, textNode);
+        }
    }

 }
@@ -119,8 +121,7 @@ export function htmlPlugin(htmlOutput) {
                }
            }
        }, {
-            decorations: v => v.decorations,
-
+            decorations: v => v.decorations
        }
    );