/*	hyperlinks:	*/
a {
    text-decoration: none;
}
a:hover {
//  text-decoration: underline;
    background-color: #DDF
}

/*	main elements:	*/
div.navheader table th {
    font-size: 100%;
/*  font-family: Helvetica;
    font-weight: Bold;
    color: #444444 */
}
/* div.navfooter table td {
    font-size: 100%;
    font-family: Helvetica;
    font-weight: Bold;
    color: #444444
} */
div.chapter div.titlepage h2 {
    font-size: 180%;
/*  font-family: Helvetica;
    font-weight: Bold;
    color: #444444 */
}
div.section div.titlepage h2.title {
    font-size: 120%;
/*  font-family: Helvetica;
    font-weight: Bold;
    color: #444444 */
}
div.section div.titlepage h3.title {
    font-size: 100%;
/*  font-family: Helvetica;
    font-weight: Bold;
    color: #444444 */
}

/*	examples, program listings, etc.	*/
div.blockquote, div.informalexample, .example-contents {
  background-color: #EEEEFF ;
  border: 1px solid #CCCCCC ;
}
blockquote.blockquote {
  margin: 0px;
}
pre.programlisting, pre.literallayout {
  margin-top: 4px;
  margin-bottom: 4px;
  margin-left: 20px;
}

/*	sidebars	*/
div.sidebar {
  background-color: #DDFFDD ;
  border: 1px solid #CCCCCC ;
}
div.sidebar p {
  margin-left: 20px;
  margin-right: 20px;
}

/*	inline elements	*/
.type {
    font-family: "Courier New", Courier;
    font-size: 90%;
    color: #000060;
}
.constant {
    color: #5000A0;
}
.function {
    color: #306000;
}
.code {
    color: #800050;
}
.filename {
    color: #006040;
/*  font-size: 108%; */
}
.package, .productname, .productnumber {
    font-family: "Courier New", Courier;
    font-size: 100%;
    color: #006060;
}

/* for the title line at the top of the document: */
body div span.productnumber {
    font-family: "Times New Roman", Times;
/*  font-family: default;  */
    color: #000;
}

.guibutton, .guiicon, .guilabel, .guimenu, .guimenuitem, .guisubmenu {
  font-weight: Bold;
}