/usr/share/gap/doc/ref/chooser.html is in gap-doc 4r7p5-2.
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 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 | <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en">
<head>
<title>GAPDoc Style Chooser</title>
<meta http-equiv="content-type" content="text/html; charset=UTF-8" />
<meta name="generator" content="GAPDoc2HTML" />
<link rel="stylesheet" type="text/css" href="manual.css" />
<script src="manual.js" type="text/javascript"></script>
<script type="text/javascript">
<!-- find current value of name nam in form -->
function currval(nam) {
var chform = document.forms[0].elements;
for (var i=0; chform.length > i; i++) {
if (chform[i].name == nam && chform[i].type == "radio" &&
chform[i].checked == true)
return chform[i].value;
}
return "";
}
<!-- find style from current values in form -->
function getstyle() {
var choices = ["toggle","colorprompt","tocside","font","justify"];
var style = "";
for (var i=0; choices.length > i; i++) {
var a = currval(choices[i]);
if (a.length > 0) {
if (style.length > 0)
style = style + ",";
style = style + a;
}
}
if (style.length == 0)
style = "default";
return style;
}
<!-- adjust the back link -->
function f() {
addr = window.location.search.split("=")[1];
addr = addr + "?GAPDocStyle=" + getstyle();
document.getElementsByName("backLINK")[0].href = addr;
}
function resetf() {
addr = window.location.search.split("=")[1];
addr = addr + "?GAPDocStyle=default";
document.getElementsByName("backLINK")[0].href = addr;
}
<!-- initialize form from GAPDocStyle cookie -->
function initform() {
var style = valueString(document.cookie, "GAPDocStyle");
if (style != 0 && style.length > 0 && style.length != "default") {
stlist = style.split(",");
var chform = document.forms[0].elements;
for (var i=0; chform.length > i; i++) {
if (chform[i].type == "radio") {
for (var j=0; stlist.length > j; j++) {
if (chform[i].value == stlist[j])
chform[i].checked = true;
}
}
}
}
}
</script>
</head>
<body class="chooser">
<h2>Setting preferences for GAPDoc manuals</h2>
<form name="SetGAPDocHTMLStyle" action="">
<p>
<input name="reset" type="reset" value="Reset to defaults"
onclick="javascript:resetf()"/>
</p>
<p>
Unfold subsections in menus only by mouse clicks:
<input type="radio" name="toggle" value="" checked="checked"
onclick="javascript:f()"/> no (default)
<input type="radio" name="toggle" value="toggless"
onclick="javascript:f()"/> yes
</p>
<p>
Show GAP examples as in sessions with <code>ColorPrompt(true)</code>:
<input type="radio" name="colorprompt" value="" checked="checked"
onclick="javascript:f()"/> yes
(default)
<input type="radio" name="colorprompt" value="nocolorprompt"
onclick="javascript:f()"/> no
</p>
<p>
Display side of table of contents within chapters:
<input type="radio" name="tocside" value="" checked="checked"
onclick="javascript:f()"/> right (default)
<input type="radio" name="tocside" value="lefttoc"
onclick="javascript:f()"/> left
</p>
<p>
Main document font:
<input type="radio" name="font" value="" checked="checked"
onclick="javascript:f()"/> Helvetica/sans
serif (default)
<input type="radio" name="font" value="times"
onclick="javascript:f()"/> Times/serif
</p>
<p>
Paragraph formatting:
<input type="radio" name="justify" value="" checked="checked"
onclick="javascript:f()"/> left-right
justified (default)
<input type="radio" name="justify" value="ragged"
onclick="javascript:f()"/> ragged right
</p>
</form>
<p>
<a name="backLINK" href=""><strong>Apply settings to last page.</strong></a>
</p>
<script type="text/javascript">
initform();
f();
</script>
</body>
</html>
|