def htmlHeader(output, path, serverName, query = None):
  """Writes an HTML header."""
  if path and path != '/':
    output.write('<title>%s - Status: %s</title>' % (serverName, path))
  else:
    output.write('<title>%s - Status</title>' % serverName)
  output.write('''
<style>
body,td { font-family: monospace }
.level div {
  padding-bottom: 4px;
}
.level .level {
  margin-left: 2em;
  padding: 1px 0;
}
span { color: #090; vertical-align: top }
.key { color: black; font-weight: bold }
.int, .float { color: #00c }
</style>
  ''')
  output.write('<h1 style="margin: 0">Stats</h1>')
  output.write('<h3 style="margin: 3px 0 18px">%s</h3>' % serverName)
  output.write(
      '<p><form action="#" method="GET">Filter: <input type="text" name="query" size="20" value="%s"></form></p>' %
      (query or ''))
Writes an HTML header.