/usr/share/gap/doc/tut/manual.js is in gap-doc 4r6p5-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 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 | /* manual.js Frank Lübeck */
/* This file contains a few javascript functions which allow to switch
between display styles for GAPDoc HTML manuals.
If javascript is switched off in a browser or this file in not available
in a manual directory, this is no problem. Users just cannot switch
between several styles and don't see the corresponding button.
A style with name mystyle can be added by providing two files (or only
one of them).
mystyle.js: Additional javascript code for the style, it is
read in the HTML pages after this current file.
The additional code may adjust the preprocessing function
jscontent() with is called onload of a file. This
is done by appending functions to jscontentfuncs
(jscontentfuncs.push(newfunc);).
Make sure, that your style is still usable without
javascript.
mystyle.css: CSS configuration, read after manual.css (so it can
just reconfigure a few details, or overwrite everything).
Then adjust chooser.html such that users can switch on and off mystyle.
A user can change the preferred style permanently by using the [Style]
link and choosing one. Or one can append '?GAPDocStyle=mystyle' to the URL
when loading any file of the manual (so the style can be configured in
the GAP user preferences).
*/
/* generic helper function */
function deleteCookie(nam) {
document.cookie = nam+"=;Path=/;expires=Thu, 01 Jan 1970 00:00:00 GMT";
}
/* read a value from a "nam1=val1;nam2=val2;..." string (e.g., the search
part of an URL or a cookie */
function valueString(str,nam) {
var cs = str.split(";");
for (var i=0; i < cs.length; i++) {
var pos = cs[i].search(nam+"=");
if (pos > -1) {
pos = cs[i].indexOf("=");
return cs[i].slice(pos+1);
}
}
return 0;
}
/* when a non-default style is chosen via URL or a cookie, then
the cookie is reset and the styles .js and .css files are read */
function overwriteStyle() {
/* style in URL? */
var style = valueString(window.location.search, "GAPDocStyle");
/* otherwise check cookie */
if (style == 0)
style = valueString(document.cookie, "GAPDocStyle");
if (style == 0)
return;
if (style == "default")
deleteCookie("GAPDocStyle");
else {
/* ok, we set the cookie for path "/" */
var path = "/";
/* or better like this ???
var here = window.location.pathname.split("/");
for (var i=0; i+3 < here.length; i++)
path = path+"/"+here[i];
*/
document.cookie = "GAPDocStyle="+style+";Path="+path;
/* split into names of style files */
var stlist = style.split(",");
/* read style's css and js files */
for (var i=0; i < stlist.length; i++) {
document.writeln('<link rel="stylesheet" type="text/css" href="'+
stlist[i]+'.css" />');
document.writeln('<script src="'+stlist[i]+
'.js" type="text/javascript"></script>');
}
}
}
/* this adds a "[Style]" link next to the MathJax switcher */
function addStyleLink() {
var line = document.getElementById("mathjaxlink");
var el = document.createElement("a");
var oncl = document.createAttribute("href");
var back = window.location.protocol+"//"
if (window.location.protocol == "http:") {
back = back+window.location.host;
if (window.location.port != "") {
back = back+":"+window.location.port;
}
}
back = back+window.location.pathname;
oncl.nodeValue = "chooser.html?BACK="+back;
el.setAttributeNode(oncl);
var cont = document.createTextNode(" [Style]");
el.appendChild(cont);
line.appendChild(el);
}
var jscontentfuncs = new Array();
jscontentfuncs.push(addStyleLink);
/* the default jscontent() only adds the [Style] link to the page */
function jscontent () {
for (var i=0; i < jscontentfuncs.length; i++)
jscontentfuncs[i]();
}
|