/* -*- c -*- */

body {
  text-align: justify;
  font-family: serif;
  font-size: 11pt;
}

div.maketitle h1 {
  font-size: 22pt;
  font-weight: bold;
  margin-top: 1ex;
  margin-bottom: 1ex;
}

div.maketitle div.date {
  font-weight: bold;
  margin-top: 1ex;
}

h1 {
  font-size: 18pt;
  font-weight: bold;

  margin-top: 3.5ex;
  margin-bottom: 1.5ex;
  
  border-bottom: solid medium darkblue;
  clear: both;
}

h2 {
  font-size: 14pt;
  font-weight: bold;

  margin-top: 3.25ex;
  margin-bottom: 1ex;

  border-bottom: solid thin blue;
  clear: both;
}

h3 {
  font-size: 11pt;
  font-weight: bold;
  
  margin-top: 3.25ex;
  margin-bottom: 1ex;
  clear: both;
}

h1, h2, h3 {
  page-break-after: avoid;
}


p {
  margin-top: 0pt;
  margin-bottom: 0pt;
  text-indent: 1.5em;
  line-height: 130%;
}


h1 + p, h2 + p, h3 + p, .no-indent {
  text-indent: 0pt;
}

li p {
  text-indent: 0pt;
  margin-top: 0.5ex;
  margin-bottom: 0.5ex;
}


p.toc-h1 {
  margin-top: 1ex;
  font-size: 110%;
  font-weight: bold;
}

p.toc-h2 {
  margin-top: 0.5ex;
  margin-left: 1.5em;
}

p.toc-h3 {
  margin-top: 0ex;
  margin-left: 3em;
  font-size: 90%;
}


p img {
  padding: 0;
  max-width: 100%;
}


a {
  text-decoration: none;
}

a:hover {
  text-decoration: underline;
}

img.centered {
  display: block;
  margin-left: auto;
  margin-right: auto;
}
	
img.right {
  padding: 4px;
  margin: 0 0 2px 7px;
  display: inline;
  float: right;
}

img.left {
  padding: 4px;
  margin: 0 7px 2px 0;
  display: inline;
  float: left;
}

pre, code {
  font-family: Verdana;
  font-size: 95%;
}

.feature-name {
  font-style: italic;
}

.class-name {
  color: blue;
  font-style: italic;
}

.keyword {
  color: darkblue;
  font-weight: bold;
  font-style: normal;
}

.variable {
  color: brown;
  font-style: italic;
}

.string {
  /* font-lock-string-face */
  color: black;
  font-style: italic;
}

.comment {
  color: darkred;
  font-style: normal;
}