+const HEADER: &str = "<!DOCTYPE html>
+<html>
+<head>
+ <meta charset=\"utf-8\">
+ <meta name=\"viewport\" content=\"width=device-width, initial-scale=1\">
+ <style>
+ /* h/t https://wabain.github.io/2019/10/13/css-rotated-table-header.html */
+ th, td { white-space: nowrap; }
+ th { text-align: left; font-weight: normal; }
+ table { border-collapse: collapse }
+ tr.key > th { height: 8em; vertical-align: bottom; line-height: 1 }
+ tr.key > th > div { width: 1em; }
+ tr.key > th > div > div { width: 5em; transform-origin: bottom left; transform: translateX(1em) rotate(-65deg) }
+ td { border: thin solid gray; }
+ td.numeric { text-align: right; }
+ td.yes { border: thin solid gray; background-color: gray; }
+ td.spacer { border: none; }
+ /* h/t https://stackoverflow.com/questions/5687035/css-bolding-some-text-without-changing-its-containers-size/46452396#46452396 */
+ .highlight { text-shadow: -0.06ex 0 black, 0.06ex 0 black; }
+ img { height: 1.2em; }
+ </style>
+ <script>
+ function highlight(id) { const e = document.getElementById(id); if (e) { e.classList.add( \"highlight\"); } }
+ function clear_highlight(id) { const e = document.getElementById(id); if (e) { e.classList.remove(\"highlight\"); } }
+ function h2(a, b) { highlight(a); highlight(b); }
+ function ch2(a, b) { clear_highlight(a); clear_highlight(b); }
+ </script>
+</head>
+<body>
+ <table>
+ <tbody>";
+const FOOTER: &str = " </tbody>
+ </table>
+</body>
+</html>";
+