From c240cb743eb5c6523525eb749786f8137a50edc0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hugo=20H=C3=B6rnquist?= <hugo@lysator.liu.se>
Date: Fri, 10 Jul 2020 22:56:42 +0200
Subject: Remove Javascript XML pretty printer.

---
 static/script.js | 43 -------------------------------------------
 1 file changed, 43 deletions(-)

diff --git a/static/script.js b/static/script.js
index ce2cc4d7..afbb66eb 100644
--- a/static/script.js
+++ b/static/script.js
@@ -1,46 +1,3 @@
-/* ------- XML Formatting --------------------------- */
-
-function start_tag(str) {
-    return "<span class='html-tag'>&lt;" + str + "&gt;</span>";
-}
-
-function end_tag(str) {
-    return "<span class='html-tag'>&lt;/" + str + "&gt;</span>";
-}
-
-function self_tag(str) {
-    return "<span class='html-tag'>&lt;" + str + "/&gt;</span>";
-}
-
-function istring(indent) {
-    return "".padStart(indent);
-}
-
-function pretty_print_xml(xml, indent=0) {
-    /* pretty_print_xml(xml.documentElement) */
-
-    let tag = xml.tagName;
-
-
-    if (xml.childElementCount == 0) {
-        if (xml.textContent) {
-            return istring(indent)
-                + start_tag(tag)
-                + "<b>" + xml.textContent + "</b>"
-                + end_tag(tag);
-        } else {
-            return istring(indent) + self_tag(tag);
-        }
-    } else {
-        let str = istring(indent) + start_tag(tag) + "<br/>";
-        for (let child of xml.children) {
-            str += pretty_print_xml(child, indent + 1) + "<br/>";
-        }
-        str += istring(indent) + end_tag(tag);
-        return str;
-    }
-}
-
 /* -------------------------------------------------- */
 
 function round_time (time, fraction) {
-- 
cgit v1.2.3