3
function populate_toc () {
4
var children = document.getElementsByTagName("h1").item(0).parentNode.childNodes
7
var counters = new Array()
13
/* Generate the table of contents */
14
for(var ii=0; ii<children.length; ii++){
15
var node = children.item(ii)
17
if( node.tagName == "H1" ){ iHeader = 1 }
18
if( node.tagName == "H2" ){ iHeader = 2 }
19
if( node.tagName == "H3" ){ iHeader = 3 }
20
if( node.tagName == "H4" ){ iHeader = 4 }
23
var anchor = "tocentry_" + ii
25
for(var jj=iHeader+1; jj<=4; jj++){ counters[jj] = 0 }
29
for(var jj=1; jj<=iHeader; jj++){ number += counters[jj] + "." }
31
toc += '<div style="margin-left:' + (iHeader*6) + 'ex">'
32
toc += '<a href="#' + anchor + '">' + number + " " + node.innerHTML
35
var a = '<a style="color:inherit" name="' + anchor + '">' + number + '</a>'
36
node.innerHTML = a + " " + node.innerHTML
39
document.getElementById("toc").innerHTML = toc
42
function number_figs () {
43
/* Number the figures in this document */
45
var spans = document.getElementsByTagName("span")
46
for(var ii=0; ii<spans.length; ii++){
47
var s = spans.item(ii)
48
if( s.className=="fig" ){
49
s.innerHTML = figcounter
55
function populate_refs () {
56
/* Fix up <cite> references */
57
var cites = document.getElementsByTagName("cite")
58
for(var ii=0; ii<cites.length; ii++){
59
var t = cites.item(ii).innerHTML
60
var h = document.getElementById(t)
63
alert("Bad reference: " + t)
68
if( h.tagName=="H1" || h.tagName=="H2"
69
|| h.tagName=="H3" || h.tagName=="H4"
71
label = h.firstChild.firstChild.data
72
label = label.substring(0, label.length-1)
74
label = h.firstChild.data
77
cites.item(ii).innerHTML = '<a href="#' + t + '">' + label + '</a>'
81
function decorate_tables () {
83
var tables = document.getElementsByTagName("table")
84
for(var ii=0; ii<tables.length; ii++){
85
var t = tables.item(ii)
86
if( t.className!="striped" ) continue
88
for(var jj=1; jj<rows.length; jj += 2){
89
rows.item(jj).style.backgroundColor = '#DDDDDD'
94
function check_for_duplicates () {
95
var aReq = new Array();
96
var ps = document.getElementsByTagName("p")
98
for(var ii=0; ii<ps.length; ii++){
100
if( p.className!="req" || !p.id ) continue;
103
alert("Duplicate requirement number: " + p.id)
109
onload = function () {
114
check_for_duplicates()