diff options
Diffstat (limited to 'doc/coq2html.js')
-rw-r--r-- | doc/coq2html.js | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/doc/coq2html.js b/doc/coq2html.js new file mode 100644 index 00000000..a840b004 --- /dev/null +++ b/doc/coq2html.js @@ -0,0 +1,24 @@ +function toggleDisplay(id) +{ + var elt = document.getElementById(id); + if (elt.style.display == 'none') { + elt.style.display = 'block'; + } else { + elt.style.display = 'none'; + } +} + +function hideAll(cls) +{ + var testClass = new RegExp("(^|s)" + cls + "(s|$)"); + var tag = tag || "*"; + var elements = document.getElementsByTagName("div"); + var current; + var length = elements.length; + for(var i=0; i<length; i++){ + current = elements[i]; + if(testClass.test(current.className)) { + current.style.display = 'none'; + } + } +} |