Improve hover highlight.

dom.js

···
         let isOID = (typeof oids === 'object') && (this.tag.isUniversal() && (this.tag.tagNumber == 0x06) || (this.tag.tagNumber == 0x0D));
         let node = DOM.tag('div', 'node');
         node.asn1 = this;
-        let head = DOM.tag('div', 'head');
+        let head = DOM.tag('span', 'head');
         head.appendChild(DOM.tag('span', 'spaces', spaces));
         const typeName = this.typeName().replace(/_/g, ' ');
         if (this.def) {

index-dark.css

···
     --preview-border-color: #b5b3b3;
     --dump-bg-color: #0c0e11;
     --dump-border-color: #505050;
+    --hover-bg-color: #505050;
 }
 h1 {
     font-weight: 200;

index.css

···
     --preview-border-color: #505050;
     --dump-bg-color: #C0C0C0;
     --dump-border-color: #E0E0E0;
+    --hover-bg-color: #E0E0E0;
 }
 html, body {
     background-color: var(--page-bg-color);
···
 }
 .node:hover > .head, .node.hover > .head {
     color: var(--link-color);
-    font-weight: bold;
+    background-color: var(--hover-bg-color);
 }
 .node:hover > .head:hover, .node.hover > .head.hover {
     color: var(--link-hover-color);