function GenToc(divname) {
  // Get the div into which the toc should be written
  var toc = document.getElementById(divname)
  if( toc == null ) return
  // Create a <ul> to hold the toc
  ul = document.createElement("ul")
  // Find all the <h2> headers
  headers = document.getElementsByTagName("h2")
  for( var i = 0; i < headers.length; ++i ) {
    header = headers[i]
    // Get the header text
    text = NodeText(header)
    if( text != null && text != "" ) {
      // Each header must have an id.
      if (header.id == "" || header.id == null)
	header.id = text.replace(/\W+/g,'_')
      var item = document.createElement("li")
      var link = document.createElement("a")
      link.href = "#" + header.id
      var textNode = document.createTextNode(text)
      link.appendChild(textNode)
      item.appendChild(link)
      ul.appendChild(item)
    }
  }
  toc.appendChild(ul)
}

// Extract the text from this node
function NodeText(node) {
  var text = ""
  for( var i = 0; i != node.childNodes.length; ++i) {
    var child = node.childNodes[i]
    if( child.nodeType == 3 )		// Node.TEXT_NODE
      text += child.nodeValue
    else
      text += NodeText(child)
  }
  return text
}