def html_header(title, page_heading=None, highlight_targets=False):
  """Write HTML file header.  TITLE and PAGE_HEADING parameters are
  expected to already by HTML-escaped if needed.  If HIGHLIGHT_TARGETS
is true, then write out a style header that causes anchor targets to be
surrounded by a red border when they are jumped to."""
  if not page_heading:
    page_heading = title
  s  = '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"\n'
  s += ' "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">\n'
  s += '<html><head>\n'
  s += '<meta http-equiv="Content-Type"'
  s += ' content="text/html; charset=UTF-8" />\n'
  if highlight_targets:
    s += '<style type="text/css">\n'
    s += ':target { border: 2px solid red; }\n'
    s += '</style>\n'
  s += '<title>%s</title>\n' % title
  s += '</head>\n\n'
  s += '<body style="text-color: black; background-color: white">\n\n'
  s += '<h1 style="text-align: center">%s</h1>\n\n' % page_heading
  s += '<hr />\n\n'
  return s