Add possibility to have multiple themes

This commit is contained in:
Guillaume Gomez
2018-01-20 21:12:00 +01:00
parent 3001ab10b9
commit 003b2bc1c6
6 changed files with 537 additions and 8 deletions

View File

@@ -122,6 +122,10 @@
}
}
document.getElementsByTagName("body")[0].style.marginTop = '45px';
var themePicker = document.getElementById("theme-picker");
if (themePicker) {
themePicker.style.position = "fixed";
}
}
function hideSidebar() {
@@ -136,6 +140,10 @@
filler.remove();
}
document.getElementsByTagName("body")[0].style.marginTop = '';
var themePicker = document.getElementById("theme-picker");
if (themePicker) {
themePicker.style.position = "absolute";
}
}
// used for special search precedence
@@ -1532,7 +1540,9 @@
ul.appendChild(li);
}
div.appendChild(ul);
sidebar.appendChild(div);
if (sidebar) {
sidebar.appendChild(div);
}
}
block("primitive", "Primitive Types");