Update appearance of external links

lib/tree-updater.rkt

@@ -235,6 +235,16 @@
                                    (eq? element-type 'use))
                                  element))))
        return-no-element]
+      ; svg icon for external links
+      [(and (eq? element-type 'a)
+            (dict-has-key? attributes 'href)
+            (not (string-contains? (car (dict-ref attributes 'href)) "wikipedia.org"))
+            (or (has-class? "extiw" attributes) (has-class? "external" attributes)))
+       `(,element-type
+         ,attributes
+         (,@children
+          (svg (@ (fill "currentColor") (width "12") (height "12") (viewBox "0 0 12 12") (class "external"))
+               (path (@ (d "M6 1h5v5L8.86 3.85 4.7 8 4 7.3l4.15-4.16zM2 3h2v1H2v6h6V8h1v2a1 1 0 0 1-1 1H2a1 1 0 0 1-1-1V4a1 1 0 0 1 1-1"))))))]
       ; exclude infobox items that are videos, and gallery items that are videos
       [(and (or (has-class? "pi-item" attributes)
                 (has-class? "wikia-gallery-item" attributes))

static/jsonp.js

@@ -65,7 +65,8 @@ async function cont() {
 		document.getElementById("content").replaceWith(imported)
 		document.title = xhr.responseXML.title
 		for (const e of xhr.responseXML.head.children) {
-			if (["LINK"].includes(e.tagName)) {
+			const alreadyImported = [...document.querySelectorAll("link[href]")].map(e => e.href)
+			if (e.tagName === "LINK" && !alreadyImported.includes(e.href)) {
 				const imported = document.importNode(e, true)
 				document.head.appendChild(imported)
 			}

static/main.css

@@ -174,13 +174,13 @@ img {
 }
 
 /* indicate wikipedia links */
-.extiw::after, .external::after {
+svg.external {
     vertical-align: super;
-    content: "[🡕]";
-    font-family: serif;
-    font-size: smaller;
 }
 .extiw[href*="wikipedia.org"]::after {
+    vertical-align: super;
+    font-family: serif;
+    font-size: smaller;
     content: "[W]";
 }