/usr/share/polymake/xml/documentation/functions.js is in polymake-common 3.2r2-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 | /*
Copyright (c) 1997-2018
Ewgenij Gawrilow, Michael Joswig (Technische Universitaet Berlin, Germany)
http://www.polymake.org
This program is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by the
Free Software Foundation; either version 2, or (at your option) any
later version: http://www.gnu.org/licenses/gpl.txt.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
===============================================================================
This file contains the JavaScript functions used in the documentation of
polymake.
*/
// make content appear or disappear upon clicking
function swap_content( span_id ) {
displayType = ( document.getElementById( span_id ).style.display == 'none' ) ? 'inline' : 'none';
styleImage = ( document.getElementById( span_id ).style.display == 'none' ) ? 'url(images/minus.png)' : 'url(images/plus.png)';
document.getElementById( span_id ).style.display = displayType;
var id; id=span_id.split(':')[1];
var icon; icon='icon:'+id;
document.getElementById( icon ).style.backgroundImage = styleImage;
}
// unfold element (and also all its ancestors)
function unfold( id ) {
var obj; obj=document.getElementById( id );
while (obj) {
if (obj.tagName=='DIV' && obj.className=='foldit') {
obj.style.display = 'inline';
id = obj.id;
var icon; icon='icon:'+id.split(':')[1];
document.getElementById( icon ).style.backgroundImage='url(images/minus.png)';
}
obj=obj.parentNode;
}
}
// executed upon loading
// fold everything (if JavaScript is activated)
function start() {
var list; list=document.getElementsByTagName("div");
for(var i=0; i< list.length; i++){
var temp;
temp=list[i];
if(temp.id && temp.className=='foldit'){
temp.style.display = 'none';
}
}
// jumps to anchor if there is one
if (location.href.split('#')[1]) {
var anchor; anchor = location.href.split('#')[1];
var span; span='span:'+anchor;
unfold(span);
}
}
|