eur-lex: add a greasemonkey script to complement pages with a TOC.

eur-lex/eur-lex_toc.user.js

@@ -0,0 +1,83 @@
+// ==UserScript==
+// @name        eur-lex toc
+// @namespace   eur-lex
+// @include     http://eur-lex.europa.eu/*
+// @version     1
+// @grant       none 
+// ==/UserScript==
+
+var style = document.createElement('style');
+style.type = 'text/css';
+style.innerHTML = '\
+#the-toc-this-website-lacks {\
+  position: fixed;\
+  top: 0em;\
+  left: 0em;\
+  height: 100%;\
+  overflow-y: auto;\
+  direction: rtl;\
+  white-space: nowrap;\
+}\
+#the-toc-this-website-lacks > button {\
+  display: block;\
+}\
+#the-toc-this-website-lacks > div {\
+  direction: ltr;\
+  overflow-x: auto;\
+}\
+#the-toc-this-website-lacks li {\
+  padding: 0.5em;\
+  margin: 0.5em;\
+  border-radius: 0.2em;\
+}\
+';
+
+var toc = document.createElement('div');
+var toc_ltr = document.createElement('div');
+var fold_button = document.createElement('button');
+var ol = document.createElement('ol');
+
+var article_titles = document.evaluate("//p[@class='ti-art']",
+  document, null, XPathResult.ORDERED_NODE_SNAPSHOT_TYPE, null);
+
+var buf = "";
+
+for (var i = 0; i < article_titles.snapshotLength; i++) {
+  var id = article_titles.snapshotItem(i);
+  var title = id.nextElementSibling;
+  
+  var n = id.textContent.replace(/Article /, '');
+  
+  id.id = 'article-' + n;
+  
+  var li = document.createElement('li');
+  var a = document.createElement('a');
+  a.href = '#article-' + n;
+  a.textContent = title.textContent;
+  li.appendChild(a);
+  ol.appendChild(li);
+}
+
+fold_button.textContent = "(Un)Fold TOC";
+toc.id = 'the-toc-this-website-lacks';
+
+fold_button.onclick = (function() {
+  var folded = false;
+  return function() {
+    var width = "";
+    folded = ! folded;
+    if (folded) {
+      width = "width: 16em;";
+    }
+    else {
+      width = "";
+    }
+    toc.style = width;;
+  }
+})();
+
+toc_ltr.appendChild(fold_button);
+toc_ltr.appendChild(ol);
+toc.appendChild(toc_ltr);
+document.getElementsByTagName('body')[0].appendChild(toc);
+document.getElementsByTagName('head')[0].appendChild(style);